src/HOL/Main.thy
changeset 44918 6a80fbc4e72c
parent 44860 56101fa00193
child 45990 b7b905b23b2a
     1.1 --- a/src/HOL/Main.thy	Tue Sep 13 13:17:52 2011 +0200
     1.2 +++ b/src/HOL/Main.thy	Tue Sep 13 16:21:48 2011 +0200
     1.3 @@ -11,17 +11,4 @@
     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_Lattices.Inf_bool_def [simp del]
    1.18 -declare Complete_Lattices.Sup_bool_def [simp del]
    1.19 -
    1.20  end