equal
deleted
inserted
replaced
9 writeln"Root file for FOLP examples"; |
9 writeln"Root file for FOLP examples"; |
10 |
10 |
11 proof_timing := true; |
11 proof_timing := true; |
12 |
12 |
13 time_use "ex/intro.ML"; |
13 time_use "ex/intro.ML"; |
14 time_use_thy "ex/nat"; |
14 time_use_thy "ex/Nat"; |
15 time_use "ex/foundn.ML"; |
15 time_use "ex/foundn.ML"; |
16 |
16 |
17 writeln"\n** Intuitionistic examples **\n"; |
17 writeln"\n** Intuitionistic examples **\n"; |
18 time_use "ex/int.ML"; |
18 time_use "ex/int.ML"; |
19 |
19 |
22 time_use "ex/quant.ML"; |
22 time_use "ex/quant.ML"; |
23 commit(); |
23 commit(); |
24 |
24 |
25 writeln"\n** Classical examples **\n"; |
25 writeln"\n** Classical examples **\n"; |
26 time_use "ex/cla.ML"; |
26 time_use "ex/cla.ML"; |
27 time_use_thy "ex/if"; |
27 time_use_thy "ex/If"; |
28 |
28 |
29 val thy = FOLP.thy and tac = Cla.fast_tac FOLP_cs 1; |
29 val thy = FOLP.thy and tac = Cla.fast_tac FOLP_cs 1; |
30 time_use "ex/prop.ML"; |
30 time_use "ex/prop.ML"; |
31 time_use "ex/quant.ML"; |
31 time_use "ex/quant.ML"; |
32 |
32 |