--- a/src/HOL/Real/PReal.thy Thu Nov 01 21:12:13 2001 +0100
+++ b/src/HOL/Real/PReal.thy Fri Nov 02 17:55:24 2001 +0100
@@ -28,16 +28,16 @@
defs
preal_add_def
- "R + S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x + y})"
+ "R + S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x + y})"
preal_mult_def
- "R * S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x * y})"
+ "R * S == Abs_preal({w. ? x: Rep_preal(R). ? y: Rep_preal(S). w = x * y})"
preal_less_def
- "R < (S::preal) == Rep_preal(R) < Rep_preal(S)"
+ "R < (S::preal) == Rep_preal(R) < Rep_preal(S)"
preal_le_def
- "R <= (S::preal) == Rep_preal(R) <= Rep_preal(S)"
+ "R <= (S::preal) == Rep_preal(R) <= Rep_preal(S)"
end