move class perfect_space into RealVector.thy;
use not_open_singleton as perfect_space class axiom;
generalize some lemmas to class perfect_space;
(* Title: HOL/Import/HOL4Syntax.thy
Author: Sebastian Skalberg, TU Muenchen
*)
theory HOL4Syntax
imports HOL4Setup
uses "import_syntax.ML"
begin
ML {* HOL4ImportSyntax.setup() *}
end