explicit Syntax.tokenize, Syntax.parse;

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

simplified standard parse/unparse;

discontinued old-style Syntax.constrainC;

typed_print_translation: discontinued show_sorts argument;

misc tuning and simplification;

moved unparse material to syntax_phases.ML;

more symbol abbrevs;

renamed Standard_Syntax to Syntax_Phases;

moved decode/parse operations to standard_syntax.ML; tuned;

separate module for standard implementation of inner syntax operations;

moved Isar/local_syntax.ML to Syntax/local_syntax.ML;

merged

added "no_atp" to Cantor's paradox

renamed "const_args" option value to "args"

temporarily allow useless encoding of helper facts (e.g. fequal_def) instead of throwing exception

updated instructions

minor doc edits

killed unimplemented type encoding "preds"

remove debugging code

removing bounded_forall code equation for characters when loading Code_Char

deriving bounded_forall instances in quickcheck_exhaustive

generalizing ensure_sort_datatype for bounded_forall instances

document "type_sys" option

if "monomorphize" is enabled, mangle the type information in the names by default

use standard tables with standard argument order;

discontinued special treatment of structure Parser -- directly accessible;

discontinued special treatment of structure Ast: no pervasive content, no inclusion in structure Syntax;

more precise propagation of reports/results through some inner syntax layers; misc reorganization;

accumulate parsetrees in canonical reverse order;