doc-src/IsarRef/Thy/ROOT.ML
changeset 48610 0095de9e9da0
parent 48609 0090fab725e3
child 48611 b34ff75c23a7
--- a/doc-src/IsarRef/Thy/ROOT.ML	Mon Jul 30 17:03:24 2012 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,19 +0,0 @@
-quick_and_dirty := true;
-
-use_thys [
-  "Preface",
-  "Synopsis",
-  "Framework",
-  "First_Order_Logic",
-  "Outer_Syntax",
-  "Document_Preparation",
-  "Spec",
-  "Proof",
-  "Inner_Syntax",
-  "Misc",
-  "Generic",
-  "HOL_Specific",
-  "Quick_Reference",
-  "Symbols",
-  "ML_Tactic"
-];