--- a/src/HOL/Main.thy Sat Aug 20 01:21:22 2011 +0200
+++ b/src/HOL/Main.thy Sat Aug 20 01:33:58 2011 +0200
@@ -11,4 +11,17 @@
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_Lattice.Inf_bool_def [simp del]
+declare Complete_Lattice.Sup_bool_def [simp del]
+
end