src/HOL/Auth/Public.thy

--- a/src/HOL/Auth/Public.thy	Tue Mar 22 16:30:43 2005 +0100
+++ b/src/HOL/Auth/Public.thy	Tue Mar 22 16:31:51 2005 +0100
@@ -55,10 +55,6 @@
     "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 (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