src/HOL/Real/Ferrante_Rackoff.thy
changeset 22929 e6b6f8dd03e9
parent 22917 3c56b12fd946
child 23319 173f4d2dedc2
     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"