diff -r a0e6bda62b7b -r 3d51fbf81c17 src/HOL/Real/RealDef.ML
--- a/src/HOL/Real/RealDef.ML	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Real/RealDef.ML	Fri Oct 05 21:52:39 2001 +0200
@@ -130,7 +130,7 @@
 by (asm_full_simp_tac (simpset() addsimps [real_minus_minus]) 1);
 qed "inj_real_minus";
 
-Goalw [real_zero_def] "-0 = (0::real)";
+Goalw [real_zero_def] "- 0 = (0::real)";
 by (simp_tac (simpset() addsimps [real_minus]) 1);
 qed "real_minus_zero";