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