src/HOL/ROOT

--- a/src/HOL/ROOT	Mon Jun 08 15:09:57 2020 +0200
+++ b/src/HOL/ROOT	Mon Jun 08 21:38:41 2020 +0200
@@ -13,6 +13,24 @@
     "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.
@@ -631,7 +649,6 @@
     Lagrange
     List_to_Set_Comprehension_Examples
     LocaleTest2
-    "ML"
     MergeSort
     MonoidGroup
     Multiquote
@@ -653,7 +670,6 @@
     Rewrite_Examples
     SOS
     SOS_Cert
-    Seq
     Serbian
     Set_Comprehension_Pointfree_Examples
     Set_Theory
@@ -687,10 +703,6 @@
   "
   options [quick_and_dirty]
   theories
-    Knaster_Tarski
-    Peirce
-    Drinker
-    Cantor
     Structured_Statements
     Basic_Logic
     Expr_Compiler