author | nipkow |
Mon, 06 Aug 2001 13:43:24 +0200 | |
changeset 11464 | ddea204de5bc |
parent 11380 | e76366922751 |
child 12776 | 249600a63ba9 |
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 |
||
1351 | 9 |
time_use_thy "AC_Equiv"; |
1123 | 10 |
|
1351 | 11 |
time_use_thy "WO6_WO1"; |
5471 | 12 |
time_use_thy "WO1_WO7"; |
1123 | 13 |
|
1351 | 14 |
time_use "AC7_AC9.ML"; |
992 | 15 |
|
1351 | 16 |
time_use_thy "WO1_AC"; |
17 |
time_use_thy "AC1_WO2"; |
|
1123 | 18 |
|
1351 | 19 |
time_use_thy "AC15_WO6"; |
1123 | 20 |
|
1351 | 21 |
time_use_thy "WO2_AC16"; |
22 |
time_use_thy "AC16_WO4"; |
|
1123 | 23 |
|
1351 | 24 |
time_use_thy "AC17_AC1"; |
1071 | 25 |
|
1351 | 26 |
time_use_thy "AC18_AC19"; |
1196 | 27 |
|
1351 | 28 |
time_use_thy "DC"; |