--- a/src/HOL/Real/RealArith.ML Fri Dec 01 19:44:48 2000 +0100 +++ b/src/HOL/Real/RealArith.ML Fri Dec 01 19:53:29 2000 +0100 @@ -1,4 +1,3 @@ - (*useful??*) Goal "(z = z + w) = (w = (#0::real))"; by Auto_tac;