more explicit invented name;

minor renovation of old-style 'axioms' -- make it an alias of iterated 'axiomatization';

do not open ML structures;

modernized overloaded definitions;

standard headers;

slightly more uniform definitions -- eliminated old-style meta-equality;

eliminated old constdefs;

corrected setup for of_list

renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;

added lemma infinite_Un

Check that argument is not a 'Bound' before calling fastype_of.

typedef etc.: no constraints;

allow sort constraints in HOL/typedef;

allow sort constraints in HOL/typedef and related HOLCF variants;

OuterParse.type_args_constrained;

support type arguments with sort constraints;

typedecl: no sort constraints; prefer Name.invents over old-style Name.variant_list;

eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints;

typedecl: no sort constraints;

eliminated slightly odd typedecl_wrt in favour of explicit predeclare_constraints (which also works for recursive types); allow sort constraints; misc tuning and clarification;

Added product measure space

added type constraints to make SML/NJ happy

merged

fix Mirabelle after renaming Sledgehammer structures

merged

now use "Named_Thms" for "noatp", and renamed "noatp" to "no_atp"

renamed "ATP_Linkup" theory to "Sledgehammer"

renamed Sledgehammer structures

move Sledgehammer files in a directory of their own

merged

dropped odd interpretation of comm_monoid_mult into comm_monoid_add

lemma swap_inj_on, swap_product