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