lib/monads: coherent document structure

Now that we're producing a proof document, theory order and chapter/section nesting matters more. Signed-off-by: Gerwin Klein <[email protected]>
seL4 · Oct 12, 2023 · 52462c4 · 52462c4
1 parent 0873e0d
commit 52462c4
Show file tree

Hide file tree

Showing 6 changed files with 19 additions and 8 deletions.
diff --git a/lib/Monads/Fun_Pred_Syntax.thy b/lib/Monads/Fun_Pred_Syntax.thy
@@ -7,6 +7,8 @@
 (* Syntax for using multi-argument functions as predicates, e.g "P and Q" where P and Q are
    functions to bool, taking one or more parameters. *)
 
+chapter \<open>Function Predicate Syntax\<close>
+
 theory Fun_Pred_Syntax
 imports Main
 begin

diff --git a/lib/Monads/ROOT b/lib/Monads/ROOT
@@ -22,14 +22,7 @@ session Monads (lib) = HOL +
     trace
 
   theories
-    WPBang
-    WPFix
-    Eisbach_WP
-    WPI
-    WPC
-    WP_Pre
-    WP
-    Datatype_Schematic
+    Fun_Pred_Syntax
     Nondet_Monad
     Nondet_Lemmas
     Nondet_VCG
@@ -53,6 +46,14 @@ session Monads (lib) = HOL +
     Strengthen
     Nondet_Strengthen_Setup
     Strengthen_Demo
+    WPBang
+    WPFix
+    Eisbach_WP
+    WPI
+    WPC
+    WP_Pre
+    WP
+    Datatype_Schematic
 
   document_files
     "root.tex"
diff --git a/lib/Monads/Strengthen.thy b/lib/Monads/Strengthen.thy
@@ -4,6 +4,8 @@
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
+section \<open>Manipulating Hoare Logic Assertions\<close>
+
 theory Strengthen
 imports Main
 begin

diff --git a/lib/Monads/reader_option/Reader_Option_Monad.thy b/lib/Monads/reader_option/Reader_Option_Monad.thy
@@ -11,6 +11,8 @@
  *     Option monad while loop formalisation.
  *)
 
+chapter \<open>State Projections and Reader Option Monad\<close>
+
 theory Reader_Option_Monad
   imports
     Monad_Lib

diff --git a/lib/Monads/wp/WP.thy b/lib/Monads/wp/WP.thy
@@ -4,6 +4,8 @@
  * SPDX-License-Identifier: BSD-2-Clause
  *)
 
+section \<open>Weakest Preconditions\<close>
+
 theory WP
 imports
   WP_Pre

diff --git a/lib/Monads/wp/WP_Pre.thy b/lib/Monads/wp/WP_Pre.thy
@@ -12,6 +12,8 @@ imports
   "HOL-Eisbach.Eisbach_Tools"
 begin
 
+section \<open>Creating Schematic Preconditions\<close>
+
 ML \<open>
 structure WP_Pre = struct