src/Sequents/LK.thy
changeset 30607 c3d1590debd8
parent 28952 15a4b2cf8c34
child 41959 b460124855b8
     1.1 --- a/src/Sequents/LK.thy	Fri Mar 20 11:26:59 2009 +0100
     1.2 +++ b/src/Sequents/LK.thy	Fri Mar 20 15:24:18 2009 +0100
     1.3 @@ -226,9 +226,9 @@
     1.4  
     1.5  lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
     1.6    apply (rule_tac P = Q in cut)
     1.7 -   apply (tactic {* simp_tac (simpset () addsimps @{thms if_P}) 2 *})
     1.8 +   apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_P}) 2 *})
     1.9    apply (rule_tac P = "~Q" in cut)
    1.10 -   apply (tactic {* simp_tac (simpset() addsimps @{thms if_not_P}) 2 *})
    1.11 +   apply (tactic {* simp_tac (@{simpset} addsimps @{thms if_not_P}) 2 *})
    1.12    apply (tactic {* fast_tac LK_pack 1 *})
    1.13    done
    1.14