| changeset 8949 | d46adac29b71 |
| parent 5582 | a356fb49e69e |
| child 9214 | 9454f30eacc7 |
--- a/src/HOL/Integ/Int.thy Wed May 24 18:40:01 2000 +0200 +++ b/src/HOL/Integ/Int.thy Wed May 24 18:41:09 2000 +0200 @@ -9,6 +9,7 @@ Int = IntDef + instance int :: order (zle_refl,zle_trans,zle_anti_sym,int_less_le) +instance int :: plus_ac0 (zadd_commute,zadd_assoc,zadd_zero) instance int :: linorder (zle_linear) constdefs