equal
deleted
inserted
replaced
866 min :: "['a::ord, 'a] => 'a" |
866 min :: "['a::ord, 'a] => 'a" |
867 "min a b == (if a <= b then a else b)" |
867 "min a b == (if a <= b then a else b)" |
868 max :: "['a::ord, 'a] => 'a" |
868 max :: "['a::ord, 'a] => 'a" |
869 "max a b == (if a <= b then b else a)" |
869 "max a b == (if a <= b then b else a)" |
870 |
870 |
|
871 hide const linorder.less_eq_less.max linorder.less_eq_less.min (* FIXME !? *) |
|
872 |
871 lemma min_linorder: |
873 lemma min_linorder: |
872 "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min" |
874 "linorder.min (op \<le> \<Colon> 'a\<Colon>linorder \<Rightarrow> 'a \<Rightarrow> bool) = min" |
873 by (rule+) (simp add: min_def linorder.min_def) |
875 by (rule+) (simp add: min_def linorder.min_def) |
874 |
876 |
875 lemma max_linorder: |
877 lemma max_linorder: |