author | paulson |
Tue, 22 Mar 2005 16:31:51 +0100 | |
changeset 15616 | cdf6eeb4ac27 |
parent 15615 | d72b1867d09d |
child 15617 | 4c7bba41483a |
--- 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