src/HOL/Lattices_Big.thy
changeset 56140 ed92ce2ac88e
parent 55803 74d3fe9031d8
child 56993 e5366291d6aa
     1.1 --- a/src/HOL/Lattices_Big.thy	Thu Mar 13 17:26:22 2014 +0100
     1.2 +++ b/src/HOL/Lattices_Big.thy	Fri Mar 14 10:08:36 2014 +0100
     1.3 @@ -640,6 +640,11 @@
     1.4    shows "Max M \<le> Max N"
     1.5    using assms by (fact Max.antimono)
     1.6  
     1.7 +end
     1.8 +
     1.9 +context linorder  (* FIXME *)
    1.10 +begin
    1.11 +
    1.12  lemma mono_Min_commute:
    1.13    assumes "mono f"
    1.14    assumes "finite A" and "A \<noteq> {}"