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;