src/HOL/ROOT
changeset 61939 3c8c390a8f0a
parent 61938 e1205f814159
child 61946 844881193616
--- a/src/HOL/ROOT	Sun Dec 27 16:00:41 2015 +0100
+++ b/src/HOL/ROOT	Sun Dec 27 16:20:02 2015 +0100
@@ -624,25 +624,25 @@
   description {*
     Miscellaneous Isabelle/Isar examples.
   *}
+  options [quick_and_dirty]
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
     "../Number_Theory/Primes"
-  theories [quick_and_dirty]
-    Structured_Statements
   theories
-    Basic_Logic
+    Knaster_Tarski
+    Peirce
+    Drinker
     Cantor
     Schroeder_Bernstein
-    Drinker
+    Structured_Statements
+    Basic_Logic
     Expr_Compiler
     Fibonacci
     Group
     Group_Context
     Group_Notepad
     Hoare_Ex
-    Knaster_Tarski
     Mutilated_Checkerboard
-    Peirce
     Puzzle
     Summation
     First_Order_Logic