--- a/src/HOL/Auth/Public.thy Tue Nov 18 11:03:33 2003 +0100
+++ b/src/HOL/Auth/Public.thy Tue Nov 18 11:03:56 2003 +0100
@@ -53,9 +53,10 @@
specification (publicKey)
injective_publicKey:
"publicKey b A = publicKey c A' ==> b=c & A=A'"
- apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"])
+ apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"])
apply (auto simp add: inj_on_def split: agent.split, presburger+)
(*faster would be this:
+ apply (simp split: agent.split, auto)
apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
*)
done