summary |
shortlog |
changelog |
graph |
tags |
branches |
files |
changeset |
file |
revisions |
annotate |
diff |
raw

src/Sequents/Modal/ROOT.ML

changeset 17481 | 75166ebb619b |

parent 9000 | c20d58286a51 |

1.1 --- a/src/Sequents/Modal/ROOT.ML Sun Sep 18 14:25:48 2005 +0200 1.2 +++ b/src/Sequents/Modal/ROOT.ML Sun Sep 18 15:20:08 2005 +0200 1.3 @@ -1,21 +1,21 @@ 1.4 -(* Title: Modal/ex/ROOT 1.5 +(* Title: Modal/ex/ROOT.ML 1.6 ID: $Id$ 1.7 Author: Martin Coen 1.8 Copyright 1991 University of Cambridge 1.9 *) 1.10 1.11 writeln "\nTheorems of T\n"; 1.12 -fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2])); 1.13 +fun try s = (writeln s; prove_goal (theory "T") s (fn _=> [T_Prover.solve_tac 2])); 1.14 time_use "Tthms.ML"; 1.15 1.16 writeln "\nTheorems of S4\n"; 1.17 -fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2])); 1.18 +fun try s = (writeln s; prove_goal (theory "S4") s (fn _=> [S4_Prover.solve_tac 2])); 1.19 time_use "Tthms.ML"; 1.20 time_use "S4thms.ML"; 1.21 1.22 writeln "\nTheorems of S43\n"; 1.23 fun try s = (writeln s; 1.24 - prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE 1.25 + prove_goal (theory "S43") s (fn _=> [S43_Prover.solve_tac 2 ORELSE 1.26 S43_Prover.solve_tac 3])); 1.27 time_use "Tthms.ML"; 1.28 time_use "S4thms.ML";