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