src/Sequents/LK/ROOT.ML
changeset 21426 87ac12bed1ab
parent 17481 75166ebb619b
child 24106 f2965bf954dc
--- a/src/Sequents/LK/ROOT.ML	Mon Nov 20 21:23:12 2006 +0100
+++ b/src/Sequents/LK/ROOT.ML	Mon Nov 20 23:47:10 2006 +0100
@@ -6,7 +6,7 @@
 Examples for Classical Logic.
 *)
 
-time_use "prop.ML";
-time_use "quant.ML";
-time_use "hardquant.ML";
-time_use_thy "Nat";
+use_thy "Propositional";
+use_thy "Quantifiers";
+use_thy "Hard_Quantifiers";
+use_thy "Nat";