--- a/src/Sequents/Modal/ROOT.ML Sun Sep 18 14:25:48 2005 +0200
+++ b/src/Sequents/Modal/ROOT.ML Sun Sep 18 15:20:08 2005 +0200
@@ -1,21 +1,21 @@
-(* Title: Modal/ex/ROOT
+(* Title: Modal/ex/ROOT.ML
ID: $Id$
Author: Martin Coen
Copyright 1991 University of Cambridge
*)
writeln "\nTheorems of T\n";
-fun try s = (writeln s; prove_goal T.thy s (fn _=> [T_Prover.solve_tac 2]));
+fun try s = (writeln s; prove_goal (theory "T") s (fn _=> [T_Prover.solve_tac 2]));
time_use "Tthms.ML";
writeln "\nTheorems of S4\n";
-fun try s = (writeln s; prove_goal S4.thy s (fn _=> [S4_Prover.solve_tac 2]));
+fun try s = (writeln s; prove_goal (theory "S4") s (fn _=> [S4_Prover.solve_tac 2]));
time_use "Tthms.ML";
time_use "S4thms.ML";
writeln "\nTheorems of S43\n";
fun try s = (writeln s;
- prove_goal S43.thy s (fn _=> [S43_Prover.solve_tac 2 ORELSE
+ prove_goal (theory "S43") s (fn _=> [S43_Prover.solve_tac 2 ORELSE
S43_Prover.solve_tac 3]));
time_use "Tthms.ML";
time_use "S4thms.ML";