towards showing " in the tutorial

tuned proof in order to avoid warning message

remove unnecessary qualifiers on names

add lemma Suc_1

merged

Require "For" keyword to be followed by at least one whitespace, to avoid that identifiers starting with "For" are interpreted as traceability information

normalize defs (again, cf. 008b7858f3c0);

some context examples;

retain literal non-HHF assumptions, to facilitate re-import in Generic_Target.import_export_proof;

another attempt to avoid duplication of global vs. local syntax (reminiscent of old fork_mixfix);

export into target context (again), to retain its 'defines' (e.g. abbreviation lcoeff in theory HOL/Algebra/UnivPoly);

better drop background syntax if entity depends on parameters; more direct Type_Infer_Context.const_type instead of Syntax.check_term, which expands abbreviations (and potentially more);

more uniform abbrev vs. define;

tuned;

clarified generic_const vs. close_schematic_term;