equal
deleted
inserted
replaced
8 |
8 |
9 writeln"Root file for FOLP examples"; |
9 writeln"Root file for FOLP examples"; |
10 |
10 |
11 FOLP_build_completed; (*Cause examples to fail if FOLP did*) |
11 FOLP_build_completed; (*Cause examples to fail if FOLP did*) |
12 |
12 |
13 proof_timing := true; |
13 set proof_timing; |
14 |
14 |
15 time_use "intro.ML"; |
15 time_use "intro.ML"; |
16 time_use_thy "Nat"; |
16 time_use_thy "Nat"; |
17 time_use "foundn.ML"; |
17 time_use "foundn.ML"; |
18 |
18 |
28 time_use_thy "If"; |
28 time_use_thy "If"; |
29 |
29 |
30 val thy = FOLP.thy and tac = Cla.fast_tac FOLP_cs 1; |
30 val thy = FOLP.thy and tac = Cla.fast_tac FOLP_cs 1; |
31 time_use "prop.ML"; |
31 time_use "prop.ML"; |
32 time_use "quant.ML"; |
32 time_use "quant.ML"; |
33 |
|
34 OS.FileSys.chDir ".."; |
|
35 maketest"END: Root file for FOLP examples"; |
|