src/HOL/Main.thy

move class perfect_space into RealVector.thy;
use not_open_singleton as perfect_space class axiom;
generalize some lemmas to class perfect_space;

header {* Main HOL *}

theory Main
imports Plain Predicate_Compile Nitpick
begin

text {*
  Classical Higher-order Logic -- only ``Main'', excluding real and
  complex numbers etc.
*}

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