author wenzelm Mon, 24 Jul 2000 23:58:19 +0200 changeset 9426 d29faa6cc391 parent 9425 fd6866d90ec1 child 9427 a9c60e655107
avoid referencing thy value; lemma_prat_add_mult_mono moved here;
 src/HOL/Real/PRat.ML file | annotate | diff | comparison | revisions
```--- a/src/HOL/Real/PRat.ML	Mon Jul 24 23:57:02 2000 +0200
+++ b/src/HOL/Real/PRat.ML	Mon Jul 24 23:58:19 2000 +0200
@@ -7,7 +7,7 @@

Delrules [equalityI];

-(*** Many theorems similar to those in Integ.thy ***)
+(*** Many theorems similar to those in theory Integ ***)
(*** Proving that ratrel is an equivalence relation ***)

Goal "[| (x1::pnat) * y2 = x2 * y1; x2 * y3 = x3 * y2 |] \
@@ -38,7 +38,7 @@
by (Fast_tac 1);
qed "ratrelE_lemma";

-val [major,minor] = goal thy
+val [major,minor] = goal (the_context ())
"[| p: ratrel;  \
\     !!x1 y1 x2 y2. [| p = ((x1,y1),(x2,y2));  x1*y2 = x2*y1 \
\                    |] ==> Q |] ==> Q";
@@ -96,7 +96,7 @@
by (Asm_full_simp_tac 1);
qed "inj_prat_of_pnat";

-val [prem] = goal thy
+val [prem] = goal (the_context ())
"(!!x y. z = Abs_prat(ratrel^^{(x,y)}) ==> P) ==> P";
by (res_inst_tac [("x1","z")]
(rewrite_rule [prat_def] Rep_prat RS quotientE) 1);
@@ -443,6 +443,11 @@
qed "prat_mult_left_less2_mono1";

+Goal "!!(a1::prat). a1 < a2 ==> a1 * b + a2 * c < a2 * (b + c)";