changeset 121 | d392174734e9 |
parent 0 | a5a9c433f639 |
child 177 | 921ad94fdddb |
--- a/src/FOLP/ex/ROOT.ML Mon Nov 15 14:41:25 1993 +0100 +++ b/src/FOLP/ex/ROOT.ML Tue Nov 16 14:10:19 1993 +0100 @@ -11,7 +11,7 @@ proof_timing := true; time_use "ex/intro.ML"; -time_use_thy "ex/nat"; +time_use_thy "ex/Nat"; time_use "ex/foundn.ML"; writeln"\n** Intuitionistic examples **\n"; @@ -24,7 +24,7 @@ writeln"\n** Classical examples **\n"; time_use "ex/cla.ML"; -time_use_thy "ex/if"; +time_use_thy "ex/If"; val thy = FOLP.thy and tac = Cla.fast_tac FOLP_cs 1; time_use "ex/prop.ML";