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;

Lin_Arith.pre_tac: inherit proper simplifier context, and get rid of posthoc renaming of bound variables;

merged

context theorem is optional

added dest_comb

a simple concept for datatype invariants