# HG changeset patch
# User paulson
# Date 976700071 -3600
# Node ID 58b6cfd8ecf3bad90cfd22bd35a7fbbe2c5ef33a
# Parent  b9d43a2add79cc88f21a29f5a2bafad82de62299
working proofs up to isCont_has_Ub

diff -r b9d43a2add79 -r 58b6cfd8ecf3 src/HOL/Real/Hyperreal/Lim.ML
--- a/src/HOL/Real/Hyperreal/Lim.ML	Wed Dec 13 10:31:46 2000 +0100
+++ b/src/HOL/Real/Hyperreal/Lim.ML	Wed Dec 13 10:34:31 2000 +0100
@@ -1736,19 +1736,13 @@
 (*----------------------------------------------------------------------------*)
 (* Intermediate Value Theorem (prove contrapositive by bisection)             *)
 (*----------------------------------------------------------------------------*)
-(* proved elsewhere surely? *)
-Goal "!!P. (~P ==> ~Q) ==> Q ==> P";
-by (auto_tac (claset() addIs [ccontr],simpset()));
-qed "contrapos2";
 
-(*
-see junk.ML
 Goal "[| f(a) <= y & y <= f(b); \
 \        a <= b; \
 \        (ALL x. a <= x & x <= b --> isCont f x) \
 \     |] ==> EX x. a <= x & x <= b & f(x) = y";
-by (rtac contrapos2 1);
-by (assume_tac 2);
+by (rtac contrapos_pp 1);
+by (assume_tac 1);
 by (cut_inst_tac [("P","%(u,v). a <= u & u <= v & v <= b --> \
 \   ~(f(u) <= y & y <= f(v))")] lemma_BOLZANO2 1);
 by (Step_tac 1);
@@ -1761,8 +1755,8 @@
 by (rotate_tac 3 2);
 by (dres_inst_tac [("x","1r")] spec 2);
 by (Step_tac 2);
-by (asm_full_simp_tac (simpset() addsimps []) 2);
-by (asm_full_simp_tac (simpset() addsimps []) 2);
+by (Asm_full_simp_tac 2);
+by (Asm_full_simp_tac 2);
 by (REPEAT(blast_tac (claset() addIs [real_le_trans]) 2));
 by (REPEAT(dres_inst_tac [("x","x")] spec 1));
 by (Asm_full_simp_tac 1);
@@ -1779,13 +1773,15 @@
 by (cut_inst_tac [("R1.0","f x"),("R2.0","y")] real_linear 1);
 by (Auto_tac);
 by (dres_inst_tac [("x","ba - x")] spec 1);
-by (auto_tac (claset(),simpset() addsimps [abs_iff,real_diff_le_eq,
-       (real_diff_def RS meta_eq_to_obj_eq) RS sym,real_less_le_iff,
-       real_le_diff_eq,CLAIM "(~(x::real) <= y) = (y < x)",
+by (auto_tac (claset(),
+     simpset() 
+	       addsimps [abs_iff, real_diff_le_eq,
+       (real_diff_def RS meta_eq_to_obj_eq) RS sym,
+       real_less_le_iff, real_le_diff_eq, 
+       CLAIM "(~(x::real) <= y) = (y < x)",
        CLAIM "(-x < -y) = ((y::real) < x)",
-       CLAIM "(-(y - x)) = (x - (y::real))"]));
-by (dres_inst_tac [("z","x"),("w","ba")] real_le_anti_sym 1);
-by (assume_tac 1 THEN Asm_full_simp_tac 1);
+       CLAIM "(-(y - x)) = (x - (y::real))",
+       CLAIM "(x-y=#0) = (x = (y::real))"]));
 by (dres_inst_tac [("x","aa - x")] spec 1);
 by (case_tac "x <= aa" 1);
 by (auto_tac (claset(),simpset() addsimps [real_minus_zero_le_iff2,
@@ -1907,8 +1903,3 @@
 (*----------------------------------------------------------------------------*)
 (* Now show that it attains its upper bound                                   *)
 (*----------------------------------------------------------------------------*)
-
-
-
-
- *)
\ No newline at end of file