equal
deleted
inserted
replaced
1 (* Title: Modal/ex/ROOT |
|
2 ID: $Id$ |
|
3 Author: Martin Coen |
|
4 Copyright 1991 University of Cambridge |
|
5 *) |
|
6 |
|
7 Sequents_build_completed; (*Cause examples to fail if Sequents did*) |
|
8 |
|
9 set proof_timing; |
|
10 |
|
11 writeln "\nTheorems of T\n"; |
|
12 fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2])); |
|
13 time_use "Modal/Tthms.ML"; |
|
14 |
|
15 writeln "\nTheorems of S4\n"; |
|
16 fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2])); |
|
17 time_use "Modal/Tthms.ML"; |
|
18 time_use "Modal/S4thms.ML"; |
|
19 |
|
20 writeln "\nTheorems of S43\n"; |
|
21 fun try s = (writeln s; |
|
22 prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE |
|
23 S43_Prover.solve_tac 3])); |
|
24 time_use "Modal/Tthms.ML"; |
|
25 time_use "Modal/S4thms.ML"; |
|
26 time_use "Modal/S43thms.ML"; |
|