--- a/src/HOL/Real/PReal.ML Mon Jul 24 23:58:19 2000 +0200
+++ b/src/HOL/Real/PReal.ML Mon Jul 24 23:58:49 2000 +0200
@@ -1,4 +1,4 @@
-(* Title : PReal.ML
+(* Title : HOL/Real/PReal.ML
ID : $Id$
Author : Jacques D. Fleuriot
Copyright : 1998 University of Cambridge
@@ -449,10 +449,6 @@
qed "mem_Rep_preal_mult_iff";
(** More lemmas for preal_add_mult_distrib2 **)
-goal PRat.thy "!!(a1::prat). a1 < a2 ==> a1 * b + a2 * c < a2 * (b + c)";
-by (auto_tac (claset() addSIs [prat_add_less2_mono1,prat_mult_less2_mono1],
- simpset() addsimps [prat_add_mult_distrib2]));
-qed "lemma_prat_add_mult_mono";
Goal "[| xb: Rep_preal z1; xc: Rep_preal z2; ya: \
\ Rep_preal w; yb: Rep_preal w |] ==> \
@@ -702,7 +698,7 @@
by (rtac preal_mult_inv 1);
qed "preal_mult_inv_right";
-val [prem] = goal thy
+val [prem] = goal (the_context ())
"(!!u. z = Abs_preal(u) ==> P) ==> P";
by (cut_inst_tac [("x1","z")]
(rewrite_rule [preal_def] (Rep_preal RS Abs_preal_inverse)) 1);
@@ -783,12 +779,12 @@
by (Simp_tac 1);
qed "preal_le_refl";
-val prems = goal thy "!!i. [| i <= j; j < k |] ==> i < (k::preal)";
+val prems = goal (the_context ()) "!!i. [| i <= j; j < k |] ==> i < (k::preal)";
by (dtac preal_le_imp_less_or_eq 1);
by (fast_tac (claset() addIs [preal_less_trans]) 1);
qed "preal_le_less_trans";
-val prems = goal thy "!!i. [| i < j; j <= k |] ==> i < (k::preal)";
+val prems = goal (the_context ()) "!!i. [| i < j; j <= k |] ==> i < (k::preal)";
by (dtac preal_le_imp_less_or_eq 1);
by (fast_tac (claset() addIs [preal_less_trans]) 1);
qed "preal_less_le_trans";