src/Sequents/Modal/ROOT.ML
author wenzelm
Sun Sep 18 15:20:08 2005 +0200 (2005-09-18)
changeset 17481 75166ebb619b
parent 9000 c20d58286a51
permissions -rw-r--r--
converted to Isar theory format;
     1 (*  Title:      Modal/ex/ROOT.ML
     2     ID:         $Id$
     3     Author:     Martin Coen
     4     Copyright   1991  University of Cambridge
     5 *)
     6 
     7 writeln "\nTheorems of T\n";
     8 fun try s = (writeln s; prove_goal (theory "T") s (fn _=> [T_Prover.solve_tac 2]));
     9 time_use "Tthms.ML";
    10 
    11 writeln "\nTheorems of S4\n";
    12 fun try s = (writeln s; prove_goal (theory "S4") s (fn _=> [S4_Prover.solve_tac 2]));
    13 time_use "Tthms.ML";
    14 time_use "S4thms.ML";
    15 
    16 writeln "\nTheorems of S43\n";
    17 fun try s = (writeln s;
    18              prove_goal (theory "S43") s (fn _=> [S43_Prover.solve_tac 2 ORELSE
    19                                            S43_Prover.solve_tac 3]));
    20 time_use "Tthms.ML";
    21 time_use "S4thms.ML";
    22 time_use "S43thms.ML";