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;
wenzelm@17481
     1
(*  Title:      Modal/ex/ROOT.ML
wenzelm@6252
     2
    ID:         $Id$
wenzelm@6252
     3
    Author:     Martin Coen
wenzelm@6252
     4
    Copyright   1991  University of Cambridge
wenzelm@6252
     5
*)
wenzelm@6252
     6
wenzelm@6252
     7
writeln "\nTheorems of T\n";
wenzelm@17481
     8
fun try s = (writeln s; prove_goal (theory "T") s (fn _=> [T_Prover.solve_tac 2]));
wenzelm@6252
     9
time_use "Tthms.ML";
wenzelm@6252
    10
wenzelm@6252
    11
writeln "\nTheorems of S4\n";
wenzelm@17481
    12
fun try s = (writeln s; prove_goal (theory "S4") s (fn _=> [S4_Prover.solve_tac 2]));
wenzelm@6252
    13
time_use "Tthms.ML";
wenzelm@6252
    14
time_use "S4thms.ML";
wenzelm@6252
    15
wenzelm@6252
    16
writeln "\nTheorems of S43\n";
wenzelm@6252
    17
fun try s = (writeln s;
wenzelm@17481
    18
             prove_goal (theory "S43") s (fn _=> [S43_Prover.solve_tac 2 ORELSE
wenzelm@6252
    19
                                           S43_Prover.solve_tac 3]));
wenzelm@6252
    20
time_use "Tthms.ML";
wenzelm@6252
    21
time_use "S4thms.ML";
wenzelm@6252
    22
time_use "S43thms.ML";