--- a/src/HOL/Integ/Int.thy Fri Jun 30 21:21:11 2000 +0200
+++ b/src/HOL/Integ/Int.thy Sat Jul 01 17:52:52 2000 +0200
@@ -16,4 +16,7 @@
nat :: int => nat
"nat(Z) == if neg Z then 0 else (@ m. Z = int m)"
+defs
+ zabs_def "abs(i::int) == if i < 0 then -i else i"
+
end