src/HOL/Real/RealDef.thy
 changeset 14341 a09441bd4f1e parent 14335 9c0b5e081037 child 14348 744c868ee0b7
```--- a/src/HOL/Real/RealDef.thy	Tue Jan 06 10:38:14 2004 +0100
+++ b/src/HOL/Real/RealDef.thy	Tue Jan 06 10:40:15 2004 +0100
@@ -330,6 +330,9 @@
apply (rule someI2, auto)
done

+
+subsection{*The Real Numbers form a Field*}
+
instance real :: field
proof
fix x y z :: real
@@ -345,10 +348,13 @@
show "0 \<noteq> (1::real)" by (rule real_zero_not_eq_one)
show "x \<noteq> 0 ==> inverse x * x = 1" by (rule real_mult_inv_left)
show "y \<noteq> 0 ==> x / y = x * inverse y" by (simp add: real_divide_def)
+  assume eq: "z+x = z+y"
+    hence "(-z + z) + x = (-z + z) + y" by (simp only: eq real_add_assoc)
qed

-(** Inverse of zero!  Useful to simplify certain equations **)
+text{*Inverse of zero!  Useful to simplify certain equations*}

lemma INVERSE_ZERO: "inverse 0 = (0::real)"
apply (unfold real_inverse_def)
@@ -652,33 +658,6 @@
done
declare real_minus_zero_less_iff2 [simp]

-ML
-{*
-val real_le_def = thm "real_le_def";
-val real_diff_def = thm "real_diff_def";
-val real_divide_def = thm "real_divide_def";
-val real_of_nat_def = thm "real_of_nat_def";
-
-val preal_trans_lemma = thm"preal_trans_lemma";
-val realrel_iff = thm"realrel_iff";
-val realrel_refl = thm"realrel_refl";
-val equiv_realrel = thm"equiv_realrel";
-val equiv_realrel_iff = thm"equiv_realrel_iff";
-val realrel_in_real = thm"realrel_in_real";
-val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
-val eq_realrelD = thm"eq_realrelD";
-val inj_Rep_REAL = thm"inj_Rep_REAL";
-val inj_real_of_preal = thm"inj_real_of_preal";
-val eq_Abs_REAL = thm"eq_Abs_REAL";
-val real_minus_congruent = thm"real_minus_congruent";
-val real_minus = thm"real_minus";
-
-*}

subsection{*Properties of Less-Than Or Equals*}

@@ -1068,6 +1047,30 @@
{*
val real_abs_def = thm "real_abs_def";

+val real_le_def = thm "real_le_def";
+val real_diff_def = thm "real_diff_def";
+val real_divide_def = thm "real_divide_def";
+val real_of_nat_def = thm "real_of_nat_def";
+
+val preal_trans_lemma = thm"preal_trans_lemma";
+val realrel_iff = thm"realrel_iff";
+val realrel_refl = thm"realrel_refl";
+val equiv_realrel = thm"equiv_realrel";
+val equiv_realrel_iff = thm"equiv_realrel_iff";
+val realrel_in_real = thm"realrel_in_real";
+val inj_on_Abs_REAL = thm"inj_on_Abs_REAL";
+val eq_realrelD = thm"eq_realrelD";
+val inj_Rep_REAL = thm"inj_Rep_REAL";
+val inj_real_of_preal = thm"inj_real_of_preal";
+val eq_Abs_REAL = thm"eq_Abs_REAL";
+val real_minus_congruent = thm"real_minus_congruent";
+val real_minus = thm"real_minus";