# HG changeset patch
# User wenzelm
# Date 1336303357 -7200
# Node ID 861dc91849204e606f018716cd05b7deb1d3ff8a
# Parent  ec815d64573f451da5927c9fffdc30610afdf5b1
more accurate ROOT.ML;

diff -r ec815d64573f -r 861dc9184920 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"
 ];