# HG changeset patch
# User paulson
# Date 1069149836 -3600
# Node ID 6c418d139f743bf08c7c8a5f03a0277312e44a45
# Parent  3862336cd4bdcaab24c69279e1e3985cd42d675b
fixed a comment

diff -r 3862336cd4bd -r 6c418d139f74 src/HOL/Auth/Public.thy
--- 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