src/HOL/Real/PReal.ML

-(*  Title       : PReal.ML
+(*  Title       : HOL/Real/PReal.ML
     ID          : $Id$
     Author      : Jacques D. Fleuriot
     Copyright   : 1998  University of Cambridge
     Description : The positive reals as Dedekind sections of positive
                   rationals. Fundamentals of Abstract Analysis 

 \                                 EX y: Rep_preal(S). z = x * y)";
 by (fast_tac (claset() addSIs [mem_Rep_preal_multD,mem_Rep_preal_multI]) 1);
 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 |] ==> \
 \                  xb * ya + xc * yb: Rep_preal (z1 * w + z2 * w)";
 by (fast_tac (claset() addIs [mem_Rep_preal_addI,mem_Rep_preal_multI]) 1);

 Goal "A*pinv(A) = (preal_of_prat (prat_of_pnat (Abs_pnat 1)))";
 by (rtac (preal_mult_commute RS subst) 1);
 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);
 by (res_inst_tac [("u","Rep_preal z")] prem 1);
 by (dtac (inj_Rep_preal RS injD) 1);

 
 Goalw [preal_le_def] "w <= (w::preal)";
 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";
 
 Goal "[| i <= j; j <= k |] ==> i <= (k::preal)";