dropped dead code

polyml: default heap size is back to -H 200 (people are still using machines with < 1GB of memory; no need to workaround heap problems of polyml-5.0 anymore);

an example file for how to treat Felleisen-Hieb-style contexts in nominal

removed (cf. object_logic.ML);

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;

removed typedecl.ML (cf. object_logic.ML);

ObjectLogic.typedecl;

replaced typedecl interpretation by ObjectLogic.typedecl (based on base_sort);

simplified using sledgehammer

Chained theorems are no longer mentioned in metis calls and (if used) they prevent the output of a structured proof.

comment

(reverted to unnamed infix)

simplified interpretations

deleted looping code theorem

to_set now applies collect_mem_simproc as well.

naming policy for instances

tuned interfaces of class module

dropped dead code

dropped legacy unnamed infix

dropped implicit assumption proof

dropped legacy ml bindings

tuned titles;

moved titles;

tuned title;

tuned titles;

standard_parse_term: check ambiguous results without changing the result yet;

challenge by John Harrison: down to 12s (was 17s, was 75s);

Knaster_Tarski: turned into Isar statement, tuned proofs;