--- a/src/HOL/Real/RComplete.ML Fri Oct 05 23:58:52 2001 +0200
+++ b/src/HOL/Real/RComplete.ML Sat Oct 06 00:02:46 2001 +0200
@@ -8,7 +8,7 @@
claset_ref() := claset() delWrapper "bspec";
-Goal "x/# 2 + x/# 2 = (x::real)";
+Goal "x/2 + x/2 = (x::real)";
by (Simp_tac 1);
qed "real_sum_of_halves";