deleted a pointless comment
authorpaulson
Tue Mar 22 16:31:51 2005 +0100 (2005-03-22 ago)
changeset 15616cdf6eeb4ac27
parent 15615 d72b1867d09d
child 15617 4c7bba41483a
deleted a pointless comment
src/HOL/Auth/Public.thy
     1.1 --- a/src/HOL/Auth/Public.thy	Tue Mar 22 16:30:43 2005 +0100
     1.2 +++ b/src/HOL/Auth/Public.thy	Tue Mar 22 16:31:51 2005 +0100
     1.3 @@ -55,10 +55,6 @@
     1.4      "publicKey b A = publicKey c A' ==> b=c & A=A'"
     1.5     apply (rule exI [of _ "%b A. 2 * agent_case 0 (\<lambda>n. n + 2) 1 A + (if b then 1 else 0)"])
     1.6     apply (auto simp add: inj_on_def split: agent.split, presburger+)
     1.7 -(*faster would be this:
     1.8 -   apply (simp split: agent.split, auto)
     1.9 -   apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
    1.10 -*)
    1.11     done                       
    1.12  
    1.13