src/HOL/ROOT

     Main (global)
     Complex_Main (global)
   document_files
     "root.bib"
     "root.tex"
+
+session "HOL-Examples" in Examples = HOL +
+  description "
+    Notable Examples in Isabelle/HOL.
+  "
+  sessions
+    "HOL-Library"
+  theories
+    Knaster_Tarski
+    Peirce
+    Drinker
+    Cantor
+    Seq
+    "ML"
+  document_files
+    "root.bib"
+    "root.tex"
+
 
 session "HOL-Proofs" (timing) in Proofs = Pure +
   description "
     HOL-Main with explicit proof terms.
   "

     Intuitionistic
     Join_Theory
     Lagrange
     List_to_Set_Comprehension_Examples
     LocaleTest2
-    "ML"
     MergeSort
     MonoidGroup
     Multiquote
     NatSum
     Normalization_by_Evaluation

     Refute_Examples
     Residue_Ring
     Rewrite_Examples
     SOS
     SOS_Cert
-    Seq
     Serbian
     Set_Comprehension_Pointfree_Examples
     Set_Theory
     Simproc_Tests
     Simps_Case_Conv_Examples

   description "
     Miscellaneous Isabelle/Isar examples.
   "
   options [quick_and_dirty]
   theories
-    Knaster_Tarski
-    Peirce
-    Drinker
-    Cantor
     Structured_Statements
     Basic_Logic
     Expr_Compiler
     Fibonacci
     Group