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 ZF_build_completed; (*Make examples fail if ZF did*) |
|
10 |
8 |
11 writeln"Root file for ZF/AC"; |
9 writeln"Root file for ZF/AC"; |
12 set proof_timing; |
10 set proof_timing; |
13 |
11 |
14 time_use_thy "AC_Equiv"; |
12 time_use_thy "AC_Equiv"; |