# HG changeset patch
# User huffman
# Date 1156365872 -7200
# Node ID eba80f91e3fccf0742aee1acc5155dfe9949ce54
# Parent  f6ccfc09694a116781da12c65cc4df3f786d5a0b
speed up some proofs

diff -r f6ccfc09694a -r eba80f91e3fc src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Wed Aug 23 22:12:54 2006 +0200
+++ b/src/HOL/Hyperreal/Lim.thy	Wed Aug 23 22:44:32 2006 +0200
@@ -93,9 +93,9 @@
 lemma LIM_add:
   assumes f: "f -- a --> L" and g: "g -- a --> M"
   shows "(%x. f x + g(x)) -- a --> (L + M)"
-proof (simp add: LIM_eq, clarify)
+proof (unfold LIM_eq, clarify)
   fix r :: real
-  assume r: "0<r"
+  assume r: "0 < r"
   from LIM_D [OF f half_gt_zero [OF r]]
   obtain fs
     where fs:    "0 < fs"
@@ -111,8 +111,9 @@
     show "0 < min fs gs"  by (simp add: fs gs)
     fix x :: real
     assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
+    hence "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
     with fs_lt gs_lt
-    have "\<bar>f x - L\<bar> < r/2" and "\<bar>g x - M\<bar> < r/2" by (auto simp add: fs_lt)
+    have "\<bar>f x - L\<bar> < r/2" and "\<bar>g x - M\<bar> < r/2" by blast+
     hence "\<bar>f x - L\<bar> + \<bar>g x - M\<bar> < r" by arith
     thus "\<bar>f x + g x - (L + M)\<bar> < r"
       by (blast intro: abs_diff_triangle_ineq order_le_less_trans)
@@ -194,8 +195,9 @@
     show "0 < min fs gs"  by (simp add: fs gs)
     fix x :: real
     assume "x \<noteq> a \<and> \<bar>x-a\<bar> < min fs gs"
+    hence  "x \<noteq> a \<and> \<bar>x-a\<bar> < fs \<and> \<bar>x-a\<bar> < gs" by simp
     with fs_lt gs_lt
-    have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by (auto simp add: fs_lt)
+    have "\<bar>f x\<bar> < 1" and "\<bar>g x\<bar> < r" by blast+
     hence "\<bar>f x\<bar> * \<bar>g x\<bar> < 1*r" by (rule abs_mult_less)
     thus "\<bar>f x\<bar> * \<bar>g x\<bar> < r" by simp
   qed