1.1 --- a/src/HOL/Main.thy	Sat Aug 20 01:21:22 2011 +0200
     1.2 +++ b/src/HOL/Main.thy	Sat Aug 20 01:33:58 2011 +0200
     1.3 @@ -11,4 +11,17 @@
     1.4  
     1.5  text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
     1.6  
     1.7 +text {* Compatibility layer -- to be dropped *}
     1.8 +
     1.9 +lemma Inf_bool_def:
    1.10 +  "Inf A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    1.11 +  by (auto intro: bool_induct)
    1.12 +
    1.13 +lemma Sup_bool_def:
    1.14 +  "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    1.15 +  by auto
    1.16 +
    1.17 +declare Complete_Lattice.Inf_bool_def [simp del]
    1.18 +declare Complete_Lattice.Sup_bool_def [simp del]
    1.19 +
    1.20  end