src/HOL/Main.thy
author haftmann
Sat Aug 20 01:33:58 2011 +0200 (2011-08-20)
changeset 44324 d972b91ed09d
parent 42695 a94ad372b2f5
child 44860 56101fa00193
permissions -rw-r--r--
compatibility layer
     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_Lattice.Inf_bool_def [simp del]
    25 declare Complete_Lattice.Sup_bool_def [simp del]
    26 
    27 end