0
|
1 |
(* Title: Modal/ex/ROOT
|
|
2 |
ID: $Id$
|
|
3 |
Author: Martin Coen
|
|
4 |
Copyright 1991 University of Cambridge
|
|
5 |
*)
|
|
6 |
|
|
7 |
Modal_build_completed; (*Cause examples to fail if Modal did*)
|
|
8 |
|
|
9 |
proof_timing := true;
|
|
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 "ex/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 "ex/Tthms.ML";
|
|
18 |
time_use "ex/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 "ex/Tthms.ML";
|
|
25 |
time_use "ex/S4thms.ML";
|
|
26 |
time_use "ex/S43thms.ML";
|
|
27 |
|
1296
|
28 |
make_chart (); (*make HTML chart*)
|
|
29 |
|
0
|
30 |
maketest"END: Root file for Modal examples";
|