replaced old-style Drule.add_axiom by Specification.axiomatization

removed e-mail address from error message

merged

tuned whitespace

handle hidden polymorphism in class target (without class target syntax, though)

replaced Theory.add_axioms(_i) by more primitive Theory.add_axiom;

replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;

add_axiom: axiomatize "unconstrained" version, with explicit of_class premises; more uniform add_axiom/add_def;

Logic.mk_of_sort convenience;

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;