close context elements via Expression.cert/read_declaration; ensure visible context;

merged

added me to isatest email list

new package Lifting - initial commit

add floor/ceiling lemmas suggested by René Thiemann

made sure that " is shown in tutorial text

merged

tuned proofs

merged

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;

tuned;

more uniform theory_abbrev with const_declaration;

avoid const_declaration in aux. context (cf. locale_foundation);

clarified background_foundation vs. theory_foundation (with const_declaration);

tuned;

more general standard_declaration; generic const declaration, which is applied to nested targets (named target only);