equal
deleted
inserted
replaced
186 |
186 |
187 definition |
187 definition |
188 "(sup :: int \<Rightarrow> int \<Rightarrow> int) = max" |
188 "(sup :: int \<Rightarrow> int \<Rightarrow> int) = max" |
189 |
189 |
190 instance |
190 instance |
191 by default |
191 by standard (auto simp add: inf_int_def sup_int_def max_min_distrib2) |
192 (auto simp add: inf_int_def sup_int_def max_min_distrib2) |
|
193 |
192 |
194 end |
193 end |
195 |
194 |
196 instance int :: ordered_cancel_ab_semigroup_add |
195 instance int :: ordered_cancel_ab_semigroup_add |
197 proof |
196 proof |