# HG changeset patch
# User huffman
# Date 1315007871 25200
# Node ID d1cb7bc44370aeb1e2777fc1b5a8192e4d9b0e12
# Parent  8e6cdb9c00a7e54dffdb60cea9474dcabc97f3e2
speed up extremely slow metis proof of Sup_real_iff
(reducing total HOL compilation time by 5% on my machine)

diff -r 8e6cdb9c00a7 -r d1cb7bc44370 src/HOL/SupInf.thy
--- a/src/HOL/SupInf.thy	Fri Sep 02 16:48:30 2011 -0700
+++ b/src/HOL/SupInf.thy	Fri Sep 02 16:57:51 2011 -0700
@@ -79,7 +79,7 @@
 lemma Sup_real_iff : (*REAL_SUP_LE in HOL4*)
   fixes z :: real
   shows "X ~= {} ==> (!!x. x \<in> X ==> x \<le> z) ==> (\<exists>x\<in>X. y<x) <-> y < Sup X"
-  by (metis Sup_least Sup_upper linorder_not_le le_less_trans)
+  by (rule iffI, metis less_le_trans Sup_upper, metis Sup_least not_less)
 
 lemma Sup_eq:
   fixes a :: real