1 (* Title: ZF/AC/ROOT |
1 (* Title: ZF/AC/ROOT |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1995 University of Cambridge |
4 Copyright 1995 University of Cambridge |
5 |
5 |
6 Executes the proofs of the AC-equivalences, by Krzysztof Gr`abczewski |
6 Executes the proofs of the AC-equivalences, due to Krzysztof Gr`abczewski |
7 *) |
7 *) |
8 |
8 |
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 loadpath := [".", "AC"]; |
15 |
15 |
16 time_use_thy "WO6_WO1"; |
16 time_use_thy "AC/AC_Equiv"; |
17 |
17 |
18 (*New ones pending on ~kg10006/isabelle |
18 time_use "AC/WO1_WO6.ML"; |
19 time_use "AC10_AC11.ML"; |
19 time_use_thy "AC/WO6_WO1"; |
20 time_use "AC11_AC12.ML"; |
20 time_use "AC/WO1_WO7.ML"; |
21 time_use "AC1_AC13.ML"; |
21 time_use "AC/WO1_WO8.ML"; |
22 time_use "AC13_AC1.ML"; |
22 |
23 time_use "AC13_AC13.ML"; |
23 time_use "AC/AC0_AC1.ML"; |
24 time_use "AC13_AC14.ML"; |
24 time_use "AC/AC2_AC6.ML"; |
25 time_use "AC14_AC15.ML"; |
25 time_use "AC/AC7_AC9.ML"; |
26 time_use_thy "lemmas_AC13_AC15"; |
26 |
27 time_use_thy "AC10_AC13"; |
27 time_use_thy "AC/WO1_AC1"; |
28 time_use_thy "AC11_AC14"; |
28 time_use_thy "AC/AC1_WO2"; |
29 time_use_thy "AC12_AC15"; |
29 |
30 time_use "AC14_AC15.ML"; |
30 time_use "AC/AC10_AC15.ML"; |
31 *) |
31 time_use_thy "AC/AC15_WO6"; |
|
32 |
|
33 (* AC16 to add *) |
|
34 |
|
35 time_use "AC/AC1_AC17.ML"; |
|
36 time_use_thy "AC/AC17_AC1"; |
|
37 |
|
38 time_use_thy "AC/AC18_AC19"; |
32 |
39 |
33 writeln"END: Root file for ZF/AC"; |
40 writeln"END: Root file for ZF/AC"; |