src/Sequents/S43.thy
changeset 42814 5af15f1e2ef6
parent 41959 b460124855b8
child 51309 473303ef6e34
equal deleted inserted replaced
42813:6c841fa92fa2 42814:5af15f1e2ef6
    90 
    90 
    91 
    91 
    92 method_setup S43_solve = {*
    92 method_setup S43_solve = {*
    93   Scan.succeed (K (SIMPLE_METHOD
    93   Scan.succeed (K (SIMPLE_METHOD
    94     (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
    94     (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
    95 *} "S4 solver"
    95 *}
    96 
    96 
    97 
    97 
    98 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    98 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    99 
    99 
   100 lemma "|- []P --> P" by S43_solve
   100 lemma "|- []P --> P" by S43_solve