src/Sequents/LK/ROOT.ML
changeset 21426 87ac12bed1ab
parent 17481 75166ebb619b
child 24106 f2965bf954dc
equal deleted inserted replaced
21425:c11ab38b78a7 21426:87ac12bed1ab
     4     Copyright   1992  University of Cambridge
     4     Copyright   1992  University of Cambridge
     5 
     5 
     6 Examples for Classical Logic.
     6 Examples for Classical Logic.
     7 *)
     7 *)
     8 
     8 
     9 time_use "prop.ML";
     9 use_thy "Propositional";
    10 time_use "quant.ML";
    10 use_thy "Quantifiers";
    11 time_use "hardquant.ML";
    11 use_thy "Hard_Quantifiers";
    12 time_use_thy "Nat";
    12 use_thy "Nat";