removing duplicate code

revisiting mk_equation functions and refactoring them in exhaustive quickcheck

creating a general mk_equation_terms for the different compilations

adding an even faster compilation scheme

theory definitions for fast exhaustive quickcheck compilation

new compilation for exhaustive quickcheck

tuned;

present type variables; tuned;

unparse: more accurate markup for syntax consts, notably binders;

notation: proper markup for type constructor / constant;

tuned signature;

more accurate markup for syntax consts, notably binders which point back to the original logical entity; tuned;

discontinued Syntax.max_pri, which is not really a symbolic parameter;

CONST syntax with positions;

moved CONST syntax/translations to their proper place;

simplified Pure syntax bootstrap;

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;

type syntax as regular mixfix specification (type_ext for bootstrapping has been obsolete for many years);

moved type syntax translations to syn_trans.ML;

made SML/NJ happy (cf. 578a51fae383);

merged

merged

changing ensure_sort_datatype call in narrowing quickcheck (missed in 1491b7209e76)

prove measurable_into_infprod_algebra and measure_infprod

Rename extensional to extensionalD (extensional is also defined in FuncSet)

eliminated slightly odd Syntax.rep_syntax;

more abstract print translation;

more abstract syntax translation;

tuned;

explicit Syntax.tokenize, Syntax.parse;

eliminated odd object-oriented type_context/term_context; export ProofContext.intern_skolem;