src/Sequents/T.thy
changeset 54742 7a86358a3c0b
parent 51309 473303ef6e34
child 60770 240563fbf41d
equal deleted inserted replaced
54741:010eefa0a4f3 54742:7a86358a3c0b
    40   val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
    40   val aside_rls = [@{thm lstar0}, @{thm lstar1}, @{thm lstar2}, @{thm rstar0},
    41     @{thm rstar1}, @{thm rstar2}]
    41     @{thm rstar1}, @{thm rstar2}]
    42 )
    42 )
    43 *}
    43 *}
    44 
    44 
    45 method_setup T_solve = {* Scan.succeed (K (SIMPLE_METHOD (T_Prover.solve_tac 2))) *}
    45 method_setup T_solve = {* Scan.succeed (fn ctxt => SIMPLE_METHOD (T_Prover.solve_tac ctxt 2)) *}
    46 
    46 
    47 
    47 
    48 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    48 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
    49 
    49 
    50 lemma "|- []P --> P" by T_solve
    50 lemma "|- []P --> P" by T_solve