src/HOL/Isar_Examples/ROOT.ML

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Isar_Examples/ROOT.ML	Tue Oct 20 19:37:09 2009 +0200
@@ -0,0 +1,18 @@
+(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)
+
+no_document use_thys ["../Old_Number_Theory/Primes", "../Old_Number_Theory/Fibonacci"];
+
+use_thys [
+  "Basic_Logic",
+  "Cantor",
+  "Peirce",
+  "Drinker",
+  "Expr_Compiler",
+  "Group",
+  "Summation",
+  "Knaster_Tarski",
+  "Mutilated_Checkerboard",
+  "Puzzle",
+  "Nested_Datatype",
+  "Hoare_Ex"
+];