renamed sprop "prop#" to "prop'" -- proper identifier; eliminated spurious symbolic string bindings (logic, any etc.); hardwired special "prop" vs. "prop'" conversion; tuned;

merged

raised timeout further, for SML/NJ

discontinued special treatment of structure Lexicon;

discontinued special status of structure Printer;

discontinued special treatment of structure Syntax_Ext (formerly Syn_Ext); clarified Syntax.root;

discontinued special treatment of structure Mixfix; eliminated slightly odd no_syn convenience;

more antiquotations;

removed outdated text (cf. 84a3f86441eb);

explicit structure Syntax_Trans; discontinued old-style constrainAbsC;

tuned presentation;

report literal tokens according to parsetree head; some attempts to stack parsetrees in proper order;

simplified read_term vs. read_prop;

tuned signature;

constant =?= no longer exists (cf. 8c09e1fa24a7);

clarified sources -- removed odd comments;

tuned signature;

merged

removing decrement of cardinality in quickcheck -- counting cardinalities starts at 1

removing instantiation exhaustive for unit in Quickcheck_Exhaustive

correcting bounded_forall construction; tuned

dropped unused lemmas; proper Isar proof

further development of new Skolemizer -- make sure constructed terms have correct types and fixed a few bugs where the goal was out of sync with what we had in mind

make new Skolemizer more robust

tuned comment

discontinued user-defined token translations; tuned signature;

simplified printer context: uniform externing and static token translations;

clarified Pretty.mark; added Pretty.mark_str, Pretty.marks_str convenience;

parallel parsing of big specifications;

separate structure Term_Position; dismantled remains of structure Type_Ext;