src/HOL/Main.thy
author haftmann
Sat Sep 10 10:29:24 2011 +0200 (2011-09-10)
changeset 44860 56101fa00193
parent 44324 d972b91ed09d
child 44918 6a80fbc4e72c
permissions -rw-r--r--
renamed theory Complete_Lattice to Complete_Lattices, in accordance with Lattices, Orderings etc.
     1 header {* Main HOL *}
     2 
     3 theory Main
     4 imports Plain Predicate_Compile Nitpick
     5 begin
     6 
     7 text {*
     8   Classical Higher-order Logic -- only ``Main'', excluding real and
     9   complex numbers etc.
    10 *}
    11 
    12 text {* See further \cite{Nipkow-et-al:2002:tutorial} *}
    13 
    14 text {* Compatibility layer -- to be dropped *}
    15 
    16 lemma Inf_bool_def:
    17   "Inf A \<longleftrightarrow> (\<forall>x\<in>A. x)"
    18   by (auto intro: bool_induct)
    19 
    20 lemma Sup_bool_def:
    21   "Sup A \<longleftrightarrow> (\<exists>x\<in>A. x)"
    22   by auto
    23 
    24 declare Complete_Lattices.Inf_bool_def [simp del]
    25 declare Complete_Lattices.Sup_bool_def [simp del]
    26 
    27 end