# HG changeset patch
# User huffman
# Date 1176772418 -7200
# Node ID 704de05715b4a3018b8dd1125aae5399e23229bb
# Parent  d9be18bd7a28332e9b9aefbb33fbbe68f5660f09
lemma isCont_inv_fun is same as isCont_inverse_function

diff -r d9be18bd7a28 -r 704de05715b4 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Tue Apr 17 00:55:00 2007 +0200
+++ b/src/HOL/Hyperreal/Transcendental.thy	Tue Apr 17 03:13:38 2007 +0200
@@ -2244,21 +2244,7 @@
   shows "[| 0 < d; \<forall>z. \<bar>z - x\<bar> \<le> d --> g(f(z)) = z;  
          \<forall>z. \<bar>z - x\<bar> \<le> d --> isCont f z |]  
       ==> isCont g (f x)"
-apply (simp (no_asm) add: isCont_iff LIM_def)
-apply safe
-apply (drule_tac ?d1.0 = r in real_lbound_gt_zero)
-apply (assumption, safe)
-apply (subgoal_tac "\<forall>z. \<bar>z - x\<bar> \<le> e --> (g (f z) = z) ")
-prefer 2 apply force
-apply (subgoal_tac "\<forall>z. \<bar>z - x\<bar> \<le> e --> isCont f z")
-prefer 2 apply force
-apply (drule_tac d = e in isCont_inj_range)
-prefer 2 apply (assumption, assumption, safe)
-apply (rule_tac x = ea in exI, auto)
-apply (drule_tac x = "f (x) + xa" and P = "%y. \<bar>y - f x\<bar> \<le> ea \<longrightarrow> (\<exists>z. \<bar>z - x\<bar> \<le> e \<and> f z = y)" in spec)
-apply auto
-apply (drule sym, auto)
-done
+by (rule isCont_inverse_function)
 
 lemma isCont_inv_fun_inv:
   fixes f g :: "real \<Rightarrow> real"