src/HOL/Auth/Kerberos_BAN.thy
changeset 25112 98824cc791c0
parent 23746 a455e69c31cc
child 25134 3d4953e88449
     1.1 --- a/src/HOL/Auth/Kerberos_BAN.thy	Sat Oct 20 12:09:30 2007 +0200
     1.2 +++ b/src/HOL/Auth/Kerberos_BAN.thy	Sat Oct 20 12:09:33 2007 +0200
     1.3 @@ -133,7 +133,7 @@
     1.4  apply (rule_tac [2]
     1.5             bankerberos.Nil [THEN bankerberos.BK1, THEN bankerberos.BK2,
     1.6                               THEN bankerberos.BK3, THEN bankerberos.BK4])
     1.7 -apply (possibility, simp_all (no_asm_simp) add: used_Cons)
     1.8 +apply (possibility, simp_all (no_asm_simp) add: used_Cons neq0_conv)
     1.9  done
    1.10  
    1.11  subsection{*Lemmas for reasoning about predicate "Issues"*}