# HG changeset patch
# User paulson
# Date 1111505511 -3600
# Node ID cdf6eeb4ac27a776ec05605bc7f37a9ffa494733
# Parent  d72b1867d09dcb11f8b0a95a8f690564ae995d3e
deleted a pointless comment

diff -r d72b1867d09d -r cdf6eeb4ac27 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