src/Sequents/S43.thy
changeset 30549 d2d7874648bd
parent 30510 4120fc59dd85
child 35113 1a0c129bb2e0
equal deleted inserted replaced
30548:2eef5e71edd6 30549:d2d7874648bd
    90 )
    90 )
    91 *}
    91 *}
    92 
    92 
    93 
    93 
    94 method_setup S43_solve = {*
    94 method_setup S43_solve = {*
    95   Method.no_args (SIMPLE_METHOD
    95   Scan.succeed (K (SIMPLE_METHOD
    96     (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3))
    96     (S43_Prover.solve_tac 2 ORELSE S43_Prover.solve_tac 3)))
    97 *} "S4 solver"
    97 *} "S4 solver"
    98 
    98 
    99 
    99 
   100 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   100 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
   101 
   101