src/HOL/Main.thy
changeset 44918 6a80fbc4e72c
parent 44860 56101fa00193
child 45990 b7b905b23b2a
--- a/src/HOL/Main.thy	Tue Sep 13 13:17:52 2011 +0200
+++ b/src/HOL/Main.thy	Tue Sep 13 16:21:48 2011 +0200
@@ -11,17 +11,4 @@
 
 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
 
-text {* Compatibility layer -- to be dropped *}
-
-lemma Inf_bool_def:
-  "Inf A \<longleftrightarrow> (\<forall>x\<in>A. x)"
-  by (auto intro: bool_induct)
-
-lemma Sup_bool_def:
-  "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
-  by auto
-
-declare Complete_Lattices.Inf_bool_def [simp del]
-declare Complete_Lattices.Sup_bool_def [simp del]
-
 end