# HG changeset patch
# User paulson
# Date 1059123135 -7200
# Node ID 4cd1a7e7edac528e6d4427285e1835ce0046a662
# Parent  4d682b249437dc4f0b6de41b7094701d73d34e8b
Simplified a proof using presburger

diff -r 4d682b249437 -r 4cd1a7e7edac src/HOL/Auth/Public.thy
--- a/src/HOL/Auth/Public.thy	Thu Jul 24 18:23:17 2003 +0200
+++ b/src/HOL/Auth/Public.thy	Fri Jul 25 10:52:15 2003 +0200
@@ -52,7 +52,10 @@
     "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) 
+   apply presburger+
+(*faster would be this:
    apply (drule_tac f="%x. x mod 2" in arg_cong, simp add: mod_Suc)+
+*)
    done