cleaned up
authorhaftmann
Thu May 10 22:11:37 2007 +0200 (2007-05-10)
changeset 22929e6b6f8dd03e9
parent 22928 1feef3b54ce1
child 22930 f99617e7103f
cleaned up
src/HOL/Real/Ferrante_Rackoff.thy
     1.1 --- a/src/HOL/Real/Ferrante_Rackoff.thy	Thu May 10 22:11:36 2007 +0200
     1.2 +++ b/src/HOL/Real/Ferrante_Rackoff.thy	Thu May 10 22:11:37 2007 +0200
     1.3 @@ -140,9 +140,6 @@
     1.4    \<longrightarrow> (\<forall> y. l < y \<and> y < u \<longrightarrow> (P1 y \<or> P2 y))"
     1.5    by blast
     1.6  
     1.7 -declare Max_le_iff [simp]
     1.8 -declare Max_le_iff [simp]
     1.9 -
    1.10  lemma finite_set_intervals:
    1.11    assumes px: "P (x::real)" and lx: "l \<le> x" and xu: "x \<le> u" and linS: "l\<in> S" 
    1.12    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"