9 ZF_build_completed; (*Make examples fail if ZF did*) |
9 ZF_build_completed; (*Make examples fail if ZF did*) |
10 |
10 |
11 writeln"Root file for ZF/AC"; |
11 writeln"Root file for ZF/AC"; |
12 proof_timing := true; |
12 proof_timing := true; |
13 |
13 |
14 loadpath := [".", "AC"]; |
14 time_use_thy "AC_Equiv"; |
15 |
15 |
16 time_use_thy "AC/AC_Equiv"; |
16 time_use "WO1_WO6.ML"; |
|
17 time_use_thy "WO6_WO1"; |
|
18 time_use "WO1_WO7.ML"; |
|
19 time_use "WO1_WO8.ML"; |
17 |
20 |
18 time_use "AC/WO1_WO6.ML"; |
21 time_use "AC0_AC1.ML"; |
19 time_use_thy "AC/WO6_WO1"; |
22 time_use "AC2_AC6.ML"; |
20 time_use "AC/WO1_WO7.ML"; |
23 time_use "AC7_AC9.ML"; |
21 time_use "AC/WO1_WO8.ML"; |
|
22 |
24 |
23 time_use "AC/AC0_AC1.ML"; |
25 time_use_thy "WO1_AC"; |
24 time_use "AC/AC2_AC6.ML"; |
26 time_use_thy "AC1_WO2"; |
25 time_use "AC/AC7_AC9.ML"; |
|
26 |
27 |
27 time_use_thy "AC/WO1_AC"; |
28 time_use "AC10_AC15.ML"; |
28 time_use_thy "AC/AC1_WO2"; |
29 time_use_thy "AC15_WO6"; |
29 |
30 |
30 time_use "AC/AC10_AC15.ML"; |
31 time_use_thy "WO2_AC16"; |
31 time_use_thy "AC/AC15_WO6"; |
32 time_use_thy "AC16_WO4"; |
32 |
33 |
33 time_use_thy "AC/WO2_AC16"; |
34 time_use "AC1_AC17.ML"; |
34 time_use_thy "AC/AC16_WO4"; |
35 time_use_thy "AC17_AC1"; |
35 |
36 |
36 time_use "AC/AC1_AC17.ML"; |
37 time_use_thy "AC18_AC19"; |
37 time_use_thy "AC/AC17_AC1"; |
|
38 |
38 |
39 time_use_thy "AC/AC18_AC19"; |
39 time_use_thy "DC"; |
40 |
|
41 time_use_thy "AC/DC"; |
|
42 |
|
43 make_chart (); (*make HTML chart*) |
|
44 |
40 |
45 writeln"END: Root file for ZF/AC"; |
41 writeln"END: Root file for ZF/AC"; |