# HG changeset patch
# User haftmann
# Date 1178827897 -7200
# Node ID e6b6f8dd03e9811639c55589f1a7bb61dabf2491
# Parent  1feef3b54ce1c984888f594e880e349268cbce3c
cleaned up

diff -r 1feef3b54ce1 -r e6b6f8dd03e9 src/HOL/Real/Ferrante_Rackoff.thy
--- a/src/HOL/Real/Ferrante_Rackoff.thy	Thu May 10 22:11:36 2007 +0200
+++ b/src/HOL/Real/Ferrante_Rackoff.thy	Thu May 10 22:11:37 2007 +0200
@@ -140,9 +140,6 @@
   \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
   by blast
 
-declare Max_le_iff [simp]
-declare Max_le_iff [simp]
-
 lemma finite_set_intervals:
   assumes px: "P (x::real)" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" 
   and uinS: "u \<in> S" and fS:"finite S" and lS: "\<forall> x\<in> S. l \<le> x" and Su: "\<forall> x\<in> S. x \<le> u"