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";