equal
deleted
inserted
replaced
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, due to Krzysztof Grabczewski |
6 Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski |
7 *) |
7 *) |
8 |
|
9 writeln"Root file for ZF/AC"; |
|
10 set proof_timing; |
|
11 |
8 |
12 time_use_thy "AC_Equiv"; |
9 time_use_thy "AC_Equiv"; |
13 |
10 |
14 time_use "WO1_WO6.ML"; |
11 time_use "WO1_WO6.ML"; |
15 time_use_thy "WO6_WO1"; |
12 time_use_thy "WO6_WO1"; |
33 time_use_thy "AC17_AC1"; |
30 time_use_thy "AC17_AC1"; |
34 |
31 |
35 time_use_thy "AC18_AC19"; |
32 time_use_thy "AC18_AC19"; |
36 |
33 |
37 time_use_thy "DC"; |
34 time_use_thy "DC"; |
38 |
|
39 writeln"END: Root file for ZF/AC"; |
|