--- a/src/HOL/Real/RealOrd.ML Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Real/RealOrd.ML Fri Oct 05 21:52:39 2001 +0200
@@ -230,7 +230,7 @@
Goal "EX (x::real). x < y";
by (rtac (real_add_zero_right RS subst) 1);
-by (res_inst_tac [("x","y + (-1r)")] exI 1);
+by (res_inst_tac [("x","y + (- 1r)")] exI 1);
by (auto_tac (claset() addSIs [real_add_less_mono2],
simpset() addsimps [real_minus_zero_less_iff2, real_zero_less_one]));
qed "real_less_Ex";
@@ -269,7 +269,7 @@
symmetric real_one_def]) 1);
qed "real_of_posnat_one";
-Goalw [real_of_posnat_def] "real_of_posnat 1' = 1r + 1r";
+Goalw [real_of_posnat_def] "real_of_posnat (Suc 0) = 1r + 1r";
by (simp_tac (simpset() addsimps [real_of_preal_def,real_one_def,
pnat_two_eq,real_add,prat_of_pnat_add RS sym,
preal_of_prat_add RS sym] @ pnat_add_ac) 1);
@@ -306,7 +306,7 @@
by (simp_tac (simpset() addsimps [real_of_posnat_one]) 1);
qed "real_of_nat_zero";
-Goalw [real_of_nat_def] "real (1') = 1r";
+Goalw [real_of_nat_def] "real (Suc 0) = 1r";
by (simp_tac (simpset() addsimps [real_of_posnat_two, real_add_assoc]) 1);
qed "real_of_nat_one";
Addsimps [real_of_nat_zero, real_of_nat_one];