src/HOL/Integ/Integ.thy

--- a/src/HOL/Integ/Integ.thy	Wed Sep 23 10:17:11 1998 +0200
+++ b/src/HOL/Integ/Integ.thy	Wed Sep 23 10:25:37 1998 +0200
@@ -12,7 +12,7 @@
 instance int :: linorder (zle_linear)
 
 constdefs
-  zmagnitude  :: int => nat
-  "zmagnitude(Z) == @m. Z = $# m | -Z = $# m"
+  nat_of  :: int => nat
+  "nat_of(Z) == @m. Z = $# m | -Z = $# m"
 
 end