author | paulson |
Fri, 03 Jan 1997 15:01:55 +0100 | |
changeset 2469 | b50b8c0eec01 |
parent 1461 | 6bcb44e4d6e5 |
child 4446 | 097004a470fb |
permissions | -rw-r--r-- |
1461 | 1 |
(* Title: ZF/AC/ROOT |
992 | 2 |
ID: $Id$ |
1461 | 3 |
Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
992 | 4 |
Copyright 1995 University of Cambridge |
5 |
||
1208
bc3093616ba4
Ran expandshort and corrected spelling of Grabczewski
paulson
parents:
1196
diff
changeset
|
6 |
Executes the proofs of the AC-equivalences, due to Krzysztof Grabczewski |
992 | 7 |
*) |
8 |
||
1461 | 9 |
ZF_build_completed; (*Make examples fail if ZF did*) |
992 | 10 |
|
11 |
writeln"Root file for ZF/AC"; |
|
12 |
proof_timing := true; |
|
13 |
||
1351 | 14 |
time_use_thy "AC_Equiv"; |
1123 | 15 |
|
1351 | 16 |
time_use "WO1_WO6.ML"; |
17 |
time_use_thy "WO6_WO1"; |
|
18 |
time_use "WO1_WO7.ML"; |
|
19 |
time_use "WO1_WO8.ML"; |
|
1123 | 20 |
|
1351 | 21 |
time_use "AC0_AC1.ML"; |
22 |
time_use "AC2_AC6.ML"; |
|
23 |
time_use "AC7_AC9.ML"; |
|
992 | 24 |
|
1351 | 25 |
time_use_thy "WO1_AC"; |
26 |
time_use_thy "AC1_WO2"; |
|
1123 | 27 |
|
1351 | 28 |
time_use "AC10_AC15.ML"; |
29 |
time_use_thy "AC15_WO6"; |
|
1123 | 30 |
|
1351 | 31 |
time_use_thy "WO2_AC16"; |
32 |
time_use_thy "AC16_WO4"; |
|
1123 | 33 |
|
1351 | 34 |
time_use "AC1_AC17.ML"; |
35 |
time_use_thy "AC17_AC1"; |
|
1071 | 36 |
|
1351 | 37 |
time_use_thy "AC18_AC19"; |
1196 | 38 |
|
1351 | 39 |
time_use_thy "DC"; |
1296 | 40 |
|
992 | 41 |
writeln"END: Root file for ZF/AC"; |