--- a/src/HOL/Isar_Examples/ROOT.ML Tue Aug 07 23:38:18 2012 +0200
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,21 +0,0 @@
-(* Miscellaneous Isabelle/Isar examples for Higher-Order Logic. *)
-
-no_document use_thys ["~~/src/HOL/Library/Lattice_Syntax", "../Number_Theory/Primes"];
-
-use_thys [
- "Basic_Logic",
- "Cantor",
- "Drinker",
- "Expr_Compiler",
- "Fibonacci",
- "Group",
- "Group_Context",
- "Group_Notepad",
- "Hoare_Ex",
- "Knaster_Tarski",
- "Mutilated_Checkerboard",
- "Nested_Datatype",
- "Peirce",
- "Puzzle",
- "Summation"
-];