NEWS: authentic syntax for *all* term constants;

concrete syntax for all constructors, to workaround authentic syntax problem with domain package;

adapted to authentic syntax;

adapted to authentic syntax; misc cleanup and modernization;

adapted to authentic syntax;

authentic syntax for *all* term constants;

binder notation for default print_mode -- to avoid strange output if "xsymbols" is not active;

tuned headers; tuned proofs;

simplified syntax -- to make it work for authentic syntax;

modernized notation -- to make it work for authentic syntax;

proper markup of const syntax;

more precise dependencies;

added lemma

moved reduced Induct/SList back from AFP.

adjusted to changes in cs b987b803616d

disabled some old (fragile) isatests;

tuned settings; activated kodkodi, i.e. HOL-Nitpick_Examples;

fixed document;

eliminated opaque signature matching -- tends to cause problems with toplevel pp for abstract types;

made SML/NJ happy;

tuned;

authentic term syntax; more precise treatment of naming vs. binding; misc tuning;

Thm.def_binding;

moved ancient Drule.get_def to OldGoals.get_def;

quote the constant and theorem name with @{text}

merged

merged

local Simplifier.context; tuned tactic setup;

renamed Simplifier.theory_context to Simplifier.global_context to emphasize that this is not the real thing;

tuned message;