# HG changeset patch
# User haftmann
# Date 1313796838 -7200
# Node ID d972b91ed09d4b081392ec4375fc98f70cfe69b1
# Parent  4b5b430eb00e878e9f7945cf02672e2035d2bd12
compatibility layer

diff -r 4b5b430eb00e -r d972b91ed09d src/HOL/Main.thy
--- 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