src/HOL/IntDef.thy
changeset 23879 4776af8be741
parent 23852 3736cdf9398b
child 23950 f54c0e339061
     1.1 --- a/src/HOL/IntDef.thy	Fri Jul 20 14:27:56 2007 +0200
     1.2 +++ b/src/HOL/IntDef.thy	Fri Jul 20 14:28:01 2007 +0200
     1.3 @@ -218,7 +218,7 @@
     1.4  apply (auto simp add: zmult_zless_mono2_lemma)
     1.5  done
     1.6  
     1.7 -instance int :: minus
     1.8 +instance int :: abs
     1.9    zabs_def: "\<bar>i\<Colon>int\<bar> \<equiv> if i < 0 then - i else i" ..
    1.10  
    1.11  instance int :: distrib_lattice