replaced extend_prtabs by update_prtabs (absorb duplicates);

abbrev: PrintMode.input instead of PrintMode.internal for global version!

renamed update_list to cons_list; added proper update_list (based on Library.update);

syntax operations: turned extend'' into update'' (absorb duplicates);

renamed Symtab.update_list to Symtab.cons_list;

tuned specifications of 'notation';

added update_const_gram (avoids duplicates); tuned;

remove_prtabs: tuned, avoid excessive garbage;

update_modesyntax: based on Syntax.update_const_gram (avoids duplicates);

similar_types: uniform treatment of TFrees/TVars;

notation: based on Syntax.update_const_gram (avoids duplicates);

tuned specifications of 'notation';

removed LocalTheory.target_naming/name;

put_inductives: be permissive about multiple versions (target names are not necessarily unique); add_inductive: store info under global (!) name -- very rough approximation of the real thing;

tuned proofs; tuned document;

tuned document;

Orderings.min/max: no need to qualify consts; removed legacy ML bindings;

auto_quickcheck ref: set default in ProofGeneral/preferences only (retains responsiveness of plain tty interaction); auto_quickcheck: more messages, less complicated code;

ProofGeneral/preferences: auto_quickcheck=true;

qualified Proofterm.proofs;

@{const}: improved ProofContext.read_const does the job;

locale_const: suppress in class body as well (prevents qualified printing);

notation: improved ProofContext.read_const does the job;

updated;

replaced @{const} (allows name only) by proper @{term};

proper implementation of check phase; non-qualified names for class operations

explicit message for failed autoquickcheck

tyabbr/syntax/consts: replaced obsolete read_typ by Syntax.parse_typ/certify_typ;

avoid obsolete Sign.read_prop;

tuned proofs -- avoid implicit prems;