Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/HOL/Real/Ferrante_Rackoff.thy
changeset 22929 e6b6f8dd03e9
parent 22917 3c56b12fd946
child 23319 173f4d2dedc2 
--- 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"
isabelle