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;

removed force_strip_shyps;

lemma;

bind_thms;

proper handling of dangling sort hypotheses (at last!);

mk_simps: do *not* include Thm.strip_shyps o Drule.zero_var_indexes (asm_simp performance!);

Sign.defaultS;

strip_shyps(_warning);

mg_domain: exception DOMAIN; proper witness_sorts; removed nonempty_sort;

removed implies_intr_shyps; removed force_strip_shyps (at last!); strip_shyps: proper witness_sorts; fix_shyps: tuned for all_sorts_nonempty;

added witness_sorts, univ_witness; removed nonempty_sort; tsig: log_types, univ_witness (require rebuild_tsig!); heavily tuned;

added witness_sorts, univ_witness; removed nonempty_sort;

handle Sorts.DOMAIN;

added rems_sort;

use Drule.strip_shyps_warning; removed Thm.implies_intr_shyps;

strip_shyps_warning;

new tsig components;

more sections;

present sections;

removed extra shyps error;

added string_of: text -> string;

working snapshot with new theory "Project"

tuned;

tidied, using "warning" function and fixing the Close_locale bug

added BCV.

A new theory: a model of bytecode verification.

zero_is_mult, by symmetry

new UNITY theory: Project

AC rules for equality

zero_is_mult, by symmetry

added W_correct -- correctness of Milner's type inference algorithm W (let-free version);

documented type solver

incompatibility solver

more tidying

removed order-sorted theorems from the default claset

added 'thms_containing', 'ML_setup';

added print_thms_containing; use_mltext: strictly diag;