moved find_free to term.ML;

guess: Seq.hd; Term.find_free;

guess: Toplevel.proof;

added find_free (from Isar/proof_context.ML);

curried multiply;

induct method: fixes; tuned;

uncurried Consts.typargs;

renamed Thm.cgoal_of to Thm.cprem_of;

duplicate axioms in ATP linkup, and general fixes

tidying

called the induction principle "unsafe" instead of "test".

Skolemization by inference, but not quite finished

Explicit data structures for some Isar language elements.

tuned;

tvars_intr_list: natural argument order;

moved datatype elem to element.ML; removed unused imports function;

P.context_element, P.locale_element;

Element.context;

use existing exeption Empty;

avoid code redundancy; tuned comments;

tuned comments;

removed obsolete term set operations;

P.locale_element;

added fold_terms; added tfrees_of, frees_of; tvars_intr_list: natural argument order;

added Isar/element.ML;

Thm.varifyT': natural argument order;

added join function

allowing indentation of 'theory' keyword

simplified after_qed;

avoid prove_plain, export_plain, simplified after_qed; witness = term * thm, i.e. the original proposition with a protected fact (this achieves reliable discharge and allows facts to be slightly more general/normalized); internal assume/prove/conclude/satisfy_protected handle witness pairs accordingly; ObjectLogic.ensure_propT;