src/HOL/ROOT

     Notable Examples in Isabelle/HOL.
   "
   sessions
     "HOL-Library"
   theories
+    Adhoc_Overloading_Examples
     Ackermann
+    Cantor
+    Coherent
+    Commands
+    Drinker
+    Groebner_Examples
+    Iff_Oracle
+    Induction_Schema
     Knaster_Tarski
+    "ML"
     Peirce
-    Drinker
-    Cantor
+    Records
     Seq
-    "ML"
-    Iff_Oracle
   document_files
     "root.bib"
     "root.tex"
 
 

 session "HOL-ex" (timing) in ex = "HOL-Number_Theory" +
   description "
     Miscellaneous examples for Higher-Order Logic.
   "
   theories
-    Adhoc_Overloading_Examples
     Antiquote
     Argo_Examples
     Arith_Examples
     Ballot
     BinEx

     Classical
     Code_Binary_Nat_examples
     Code_Lazy_Demo
     Code_Timing
     Coercion_Examples
-    Coherent
-    Commands
     Computations
     Conditional_Parametricity_Examples
     Cubic_Quartic
     Datatype_Record_Examples
     Dedekind_Real

     Executable_Relation
     Execute_Choice
     Functions
     Function_Growth
     Gauge_Integration
-    Groebner_Examples
     Guess
     HarmonicSeries
     Hebrew
     Hex_Bin_Examples
     IArray_Examples
-    Induction_Schema
     Intuitionistic
     Join_Theory
     Lagrange
     List_to_Set_Comprehension_Examples
     LocaleTest2

     PresburgerEx
     Primrec
     Pythagoras
     Quicksort
     Radix_Sort
-    Records
     Reflection_Examples
     Refute_Examples
     Residue_Ring
     Rewrite_Examples
     SOS