diff -r 9e6d91f8bb73 -r 020db6ec334a src/HOL/IntDef.thy
--- a/src/HOL/IntDef.thy	Fri Aug 31 23:17:25 2007 +0200
+++ b/src/HOL/IntDef.thy	Sat Sep 01 01:21:48 2007 +0200
@@ -215,6 +215,8 @@
 
 instance int :: abs
   zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
+instance int :: sgn
+  zsgn_def: "sgn(i\<Colon>int) \<equiv> (if i=0 then 0 else if 0<i then 1 else - 1)" ..
 
 instance int :: distrib_lattice
   "inf \<equiv> min"
@@ -230,6 +232,8 @@
     by (rule zmult_zless_mono2)
   show "\<bar>i\<bar> = (if i < 0 then -i else i)"
     by (simp only: zabs_def)
+  show "sgn(i\<Colon>int) = (if i=0 then 0 else if 0<i then 1 else - 1)"
+    by (simp only: zsgn_def)
 qed
 
 lemma zless_imp_add1_zle: "w<z ==> w + (1::int) \<le> z"