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;

merged

Merged.

Corrections to locale syntax.

Update explanation of locale expressions to locale reimplementation.

Comments updated.

fixed proof

merged

fps made instance of number_ring

updated keywords with polyml-experimental;

export position_of;

dropped infix union

tuned notoriously slow metis proof

merged

dropped toy example Code_Antiq

more convenient name uniqueness

normalized imports