diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT index 5095a95aa6..5cfb076f10 100644 --- a/lib/Monads/ROOT +++ b/lib/Monads/ROOT @@ -21,33 +21,33 @@ session Monads (lib) = HOL + trace theories - Nondet_While_Loop_Rules - Trace_Monad - Reader_Option_ND - Reader_Option_VCG - Strengthen_Demo - Trace_Lemmas + WPBang + WPFix + Eisbach_WP + WPI + WPC + WP_Pre + WP Datatype_Schematic - Nondet_While_Loop_Rules_Completeness - Strengthen - Nondet_Strengthen_Setup - Reader_Option_Monad - Trace_VCG - Nondet_In_Monad - Nondet_VCG - Nondet_Sat - Nondet_More_VCG Nondet_Monad Nondet_Lemmas + Nondet_VCG + Nondet_More_VCG + Nondet_In_Monad + Nondet_Sat Nondet_Det Nondet_No_Fail Nondet_No_Throw Nondet_Empty_Fail Nondet_Monad_Equations - "wp/WPBang" - "wp/WPFix" - "wp/Eisbach_WP" - "wp/WPI" - "wp/WPC" - "wp/WP_Pre" - "wp/WP" + Nondet_While_Loop_Rules + Nondet_While_Loop_Rules_Completeness + Reader_Option_Monad + Reader_Option_ND + Reader_Option_VCG + Trace_Monad + Trace_Lemmas + Trace_VCG + Strengthen + Nondet_Strengthen_Setup + Strengthen_Demo