| changeset 54857 | 5c05f7c5f8ae |
| parent 54147 | 97a8ff4e4ac9 |
| child 54860 | 69b3e46d8fbe |
--- a/src/HOL/Orderings.thy Tue Dec 24 11:24:14 2013 +0100 +++ b/src/HOL/Orderings.thy Tue Dec 24 11:24:16 2013 +0100 @@ -1155,7 +1155,7 @@ lemma min_absorb1: "x \<le> y \<Longrightarrow> min x y = x" by (simp add: min_def) -lemma max_absorb2: "x \<le> y ==> max x y = y" +lemma max_absorb2: "x \<le> y \<Longrightarrow> max x y = y" by (simp add: max_def) lemma min_absorb2: "(y\<Colon>'a\<Colon>order) \<le> x \<Longrightarrow> min x y = y"