# HG changeset patch
# User huffman
# Date 1234970653 28800
# Node ID ca93255656a5be0ddbb2dd315e823f1b1a6d815f
# Parent  8a95050c7044fe63ec241c7e32a88e86bfbd35b7
speed up proof of exp_exists

diff -r 8a95050c7044 -r ca93255656a5 src/HOL/ex/ThreeDivides.thy
--- a/src/HOL/ex/ThreeDivides.thy	Tue Feb 17 20:45:23 2009 -0800
+++ b/src/HOL/ex/ThreeDivides.thy	Wed Feb 18 07:24:13 2009 -0800
@@ -187,9 +187,8 @@
     "nd = nlen (m div 10) \<Longrightarrow>
     m div 10 = (\<Sum>x<nd. m div 10 div 10^x mod 10 * 10^x)"
     by blast
-  have "\<exists>c. m = 10*(m div 10) + c \<and> c < 10" by presburger
-  then obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10" ..
-  then have cdef: "c = m mod 10" by arith
+  obtain c where mexp: "m = 10*(m div 10) + c \<and> c < 10"
+    and cdef: "c = m mod 10" by simp
   show "m = (\<Sum>x<nlen m. m div 10^x mod 10 * 10^x)"
   proof -
     from `Suc nd = nlen m`