fixed typo;

added signatures; tuned

abbrev: bypass full term check via ProofContext.standard_infer_types (prevents forced expansion);

simplified Consts.dest; export standard_infer_types;

simplified Consts.dest;

simplified Consts.dest; dest;

updates

avoid ML print in production code;

updated;

auto quickcheck: reduced messages;

notation works with any known constant (including fixes/abbrevs);

HOL-Statespace;

* HOL-Statespace;

restore interrupt handler on init;

abbrev: back to PrintMode.internal, which works at least half-way;

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

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;