* Isar/Pure: local results and corresponding term bindings are now subject to Hindley-Milner polymorphism (similar to ML); this accommodates incremental type-inference nicely; * Isar/Pure: new calculational elements 'moreover' and 'ultimately' support plain accumulation of results, without applying any rules yet;

support Hindley-Milner polymorphisms in results and bindings;

added 'moreover' and 'ultimately';

added \MOREOVER, \ULTIMATELY;

support Hindley-Milner polymorphisms in binds and facts; let_bind(_i): polymorphic version; moved find_free, export_wrt to Isar/proof_context.ML;

support Hindley-Milner polymorphisms in binds and facts; let_bind(_i): polymorphic version; improved warn_extra_tfrees; added find_free, export_wrt (from Isar/proof.ML);

let_bind(_i): polymorphic version;

ProofContext.find_free;

'tactic': refer to PureIsar structure;

?this: support params;

support polymorphic Vars;

tuned;

foldl_term_types: depend on term as well;

read_def_cterms: use Sign.read_def_terms;

read_def_terms (no certify yet);

export update_multi;

added tvars_intr_list;

*** empty log message ***

*** empty log message ***

mods because of weak_case_cong -> removed Action.ML twice

added weak_case_cong feature

mods because of weak_case_cong

fixed railqtoken;

-I option;

renamed 'hoare_vcg' to 'hoare';

tuned;

fixed dddot_tr;

rail token vs. terminal;

fixed term syntax;

tail token vs. terminal;