added base_sort;
added typedecl, dependent on base_sort (cf. intermediate typedecl.ML and former sign.ML, HOL/Tools/typedef_package.ML);
typedecl: recovered proper use of Syntax.type_name;
(* Title: HOL/Main.thy
ID: $Id$
*)
header {* Main HOL *}
theory Main
imports Map
begin
text {*
Theory @{text Main} includes everything. Note that theory @{text
PreList} already includes most HOL theories.
*}
ML {* val HOL_proofs = ! Proofterm.proofs *}
end