src/Sequents/LK/ROOT.ML
changeset 24106 f2965bf954dc
parent 21426 87ac12bed1ab
child 24584 01e83ffa6c54
     1.1 --- a/src/Sequents/LK/ROOT.ML	Tue Jul 31 22:21:22 2007 +0200
     1.2 +++ b/src/Sequents/LK/ROOT.ML	Tue Jul 31 23:23:28 2007 +0200
     1.3 @@ -6,7 +6,5 @@
     1.4  Examples for Classical Logic.
     1.5  *)
     1.6  
     1.7 -use_thy "Propositional";
     1.8 -use_thy "Quantifiers";
     1.9 -use_thy "Hard_Quantifiers";
    1.10 -use_thy "Nat";
    1.11 +use_thys ["Propositional", "Quantifiers", "Hard_Quantifiers", "Nat"];
    1.12 +