src/HOL/Real/RealDef.thy
changeset 11701 3d51fbf81c17
parent 10919 144ede948e58
child 11713 883d559b0b8c
--- a/src/HOL/Real/RealDef.thy	Fri Oct 05 21:50:37 2001 +0200
+++ b/src/HOL/Real/RealDef.thy	Fri Oct 05 21:52:39 2001 +0200
@@ -69,7 +69,7 @@
 defs
 
   (*overloaded*)
-  real_of_nat_def   "real n == real_of_posnat n + (-1r)"
+  real_of_nat_def   "real n == real_of_posnat n + (- 1r)"
 
   real_add_def  
   "P+Q == Abs_REAL(UN p1:Rep_REAL(P). UN p2:Rep_REAL(Q).