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;

depend on Main;

now with (weak safety) guarantees (weak progress) with Extend

bind_thm ("case_split", case_split_thm);

CollectE; AddXIs [subsetD, rev_subsetD, psubsetI];

subsetD;

update from Gertrud;

The Hahn-Banach theorem for real vectorspaces;

bind_thms;

Sign.defaultS;

Sign.of_sort;

tuned;