--- a/src/HOL/Real/PReal.ML Wed Oct 03 20:54:05 2001 +0200
+++ b/src/HOL/Real/PReal.ML Wed Oct 03 20:54:16 2001 +0200
@@ -415,7 +415,7 @@
by (Fast_tac 1);
qed "mem_Rep_preal_addI";
-Goal " z: Rep_preal(R+S) = (EX x: Rep_preal(R). \
+Goal "(z: Rep_preal(R+S)) = (EX x: Rep_preal(R). \
\ EX y: Rep_preal(S). z = x + y)";
by (fast_tac (claset() addSIs [mem_Rep_preal_addD,mem_Rep_preal_addI]) 1);
qed "mem_Rep_preal_add_iff";
@@ -434,7 +434,7 @@
by (Fast_tac 1);
qed "mem_Rep_preal_multI";
-Goal " z: Rep_preal(R*S) = (EX x: Rep_preal(R). \
+Goal "(z: Rep_preal(R*S)) = (EX x: Rep_preal(R). \
\ 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";
@@ -785,7 +785,7 @@
qed "preal_neq_iff";
(* Axiom 'order_less_le' of class 'order': *)
-Goal "(w::preal) < z = (w <= z & w ~= z)";
+Goal "((w::preal) < z) = (w <= z & w ~= z)";
by (simp_tac (simpset() addsimps [preal_less_le_iff RS sym, preal_neq_iff]) 1);
by (blast_tac (claset() addSEs [preal_less_asym]) 1);
qed "preal_less_le";