added BVC;

added mk_conj, mk_disj, mk_imp;

working snapshot (even Alloc)

most results now refer to those for "extend"

fixed lookup_theory;

fixed CHANGED_GOAL, which is used by stac

improved theory_source presentation (hook);

improved theory_source presentation;

export token_source; improved Present.theory_source;

added Space, Comment token kinds (keep actual text); source: do not filter proper;

fixed no_qed;

added Isar/obtain.ML;

improved 'fix' / Skolem interfaces;

added 'obtain' command;

tuned comment;

added prf_asm_goal;

added atomic_thesis;

The 'obtain' language element -- achieves (eliminated) existential quantification proof command level.

added undef_global_attribute, undef_local_attribute;

- Fixed bug in mk_split_pack which caused application of expansion theorem to fail because of typing reasons - Rewrote inst_lift and inst_split: now cterm_instantiate is used to instantiate theorems

fixed 'is' match;

added cert_skolem; removed declare_thm; context: removed maxidx; added maxidx_of_pair for proper unification;

export find_free;

removed ProofContext.declare_thm;

local_def_i: typ option; admit additional (fixed) type vars on rhs;

fix_i, local_def_i: typ option;

get_goal: prop; fix_i: typ option;

insert: ignore facts;

export def_sort, def_type; fix_i: typ option; init: maxidx = 0 is workaround for obscure bug in Unify.smash_unifiers;

Real/HahnBanach;