speed up extremely slow metis proof of Sup_real_iff
authorhuffman
Fri Sep 02 16:57:51 2011 -0700 (2011-09-02 ago)
changeset 44670d1cb7bc44370
parent 44669 8e6cdb9c00a7
child 44671 7f0b4515588a
speed up extremely slow metis proof of Sup_real_iff
(reducing total HOL compilation time by 5% on my machine)
src/HOL/SupInf.thy
     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