src/HOL/ROOT

--- a/src/HOL/ROOT	Sat Dec 26 16:10:00 2015 +0100
+++ b/src/HOL/ROOT	Sat Dec 26 19:27:46 2015 +0100
@@ -99,6 +99,7 @@
   theories [quick_and_dirty]
     Common_Patterns
   theories
+    Nested_Datatype
     QuoDataType
     QuoNestedDataType
     Term
@@ -548,7 +549,6 @@
     Adhoc_Overloading_Examples
     Iff_Oracle
     Coercion_Examples
-    Higher_Order_Logic
     Abstract_NAT
     Guess
     Fundefs
@@ -622,11 +622,13 @@
 
 session "HOL-Isar_Examples" in Isar_Examples = HOL +
   description {*
-    Miscellaneous Isabelle/Isar examples for Higher-Order Logic.
+    Miscellaneous Isabelle/Isar examples.
   *}
   theories [document = false]
     "~~/src/HOL/Library/Lattice_Syntax"
     "../Number_Theory/Primes"
+  theories [quick_and_dirty]
+    Structured_Statements
   theories
     Basic_Logic
     Cantor
@@ -639,12 +641,11 @@
     Hoare_Ex
     Knaster_Tarski
     Mutilated_Checkerboard
-    Nested_Datatype
     Peirce
     Puzzle
     Summation
-  theories [quick_and_dirty]
-    Structured_Statements
+    First_Order_Logic
+    Higher_Order_Logic
   document_files
     "root.bib"
     "root.tex"