1.1 --- a/src/HOL/SupInf.thy	Fri Sep 02 16:48:30 2011 -0700
     1.2 +++ b/src/HOL/SupInf.thy	Fri Sep 02 16:57:51 2011 -0700
     1.3 @@ -79,7 +79,7 @@
     1.4  lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
     1.5    fixes z :: real
     1.6    shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
     1.7 -  by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
     1.8 +  by (rule iffI, metis less_le_trans Sup_upper, metis Sup_least not_less)
     1.9  
    1.10  lemma Sup_eq:
    1.11    fixes a :: real