src/HOL/Auth/Message.thy
changeset 22424 8a5412121687
parent 21588 cd0dc678a205
child 22843 189e214845dd
     1.1 --- a/src/HOL/Auth/Message.thy	Fri Mar 09 08:45:53 2007 +0100
     1.2 +++ b/src/HOL/Auth/Message.thy	Fri Mar 09 08:45:55 2007 +0100
     1.3 @@ -323,7 +323,7 @@
     1.4  apply (induct_tac "msg")
     1.5  apply (simp_all (no_asm_simp) add: exI parts_insert2)
     1.6   txt{*MPair case: blast works out the necessary sum itself!*}
     1.7 - prefer 2 apply (blast elim!: add_leE)
     1.8 + prefer 2 apply auto apply (blast elim!: add_leE)
     1.9  txt{*Nonce case*}
    1.10  apply (rule_tac x = "N + Suc nat" in exI, auto) 
    1.11  done