Merged.

In interpretation: equations are not propagated through the hierarchy automatically.

Normalise equation only for morphism, not thm stored in theory.

Default mode of qualifiers in locale commands.

Front matter updated.

tuned;

simplified Element.activate(_i): singleton version;

tuned;

added Element.init, which unifies former activate_elem in element.ML and init_elem in locale.ML; tuned;

unified binding prefix terminology;

simplified roundup activation interface;

merged

merged

merged

second attempt for code_deps command

merged

corrected projection of required statement names

corrected check for additional type variables on rhs of code equations

not yet fruitful tex experiments with bounding boxes

simplified Locale.activate operations, using generic context; misc tuning;

renamed ProofContext.add_fixes_i to ProofContext.add_fixes, eliminated obsolete external version;

define_prefs: removed redundant Drule.gen_all, which is already part of the norm_hhf stage of Assumption.assume;

renamed ProofContext.note_thmss_i to ProofContext.note_thmss, eliminated obsolete external version;

simplified references to facts, eliminated external note_thmss;

added map_facts_refs;

tuned;

replaced add_binds(_i) by bind_terms -- internal version only;

replaced add_binds by singleton bind_term;

simplified internal locale parameters: maintain proper name and type, instead of binding and constraint;

minor tuning;