more accurate ROOT.ML;
authorwenzelm
Sun, 06 May 2012 13:22:37 +0200
changeset 47871 861dc9184920
parent 47870 ec815d64573f
child 47872 1f6f519cdb32
more accurate ROOT.ML;
src/HOL/Isar_Examples/ROOT.ML
--- a/src/HOL/Isar_Examples/ROOT.ML	Sun May 06 11:52:33 2012 +0200
+++ b/src/HOL/Isar_Examples/ROOT.ML	Sun May 06 13:22:37 2012 +0200
@@ -5,14 +5,17 @@
 use_thys [
   "Basic_Logic",
   "Cantor",
-  "Peirce",
   "Drinker",
   "Expr_Compiler",
+  "Fibonacci",
   "Group",
-  "Summation",
+  "Group_Context",
+  "Group_Notepad",
+  "Hoare_Ex",
   "Knaster_Tarski",
   "Mutilated_Checkerboard",
+  "Nested_Datatype",
+  "Peirce",
   "Puzzle",
-  "Nested_Datatype",
-  "Hoare_Ex"
+  "Summation"
 ];