2007-08-17 ago compress: proper check_thy;
2007-08-03 ago replaced Theory.self_ref by Theory.check_thy, which now produces a checked ref;
2007-07-11 ago Added function norm_proof for normalizing the proof term
2007-07-08 ago thm tag: list;
2007-07-05 ago added type conv;
2007-06-25 ago added eta_long_conversion;
2007-06-08 ago Adapted Proofterm.bicompose_proof to Larry's changes in
2007-05-31 ago simplified/unified list fold;
2007-05-10 ago added dest_fun/fun2/arg1;
2007-04-14 ago removed obsolete read_ctyp, read_def_cterm;
2007-04-04 ago rep_thm/cterm/ctyp: removed obsolete sign field;
2007-04-04 ago improved exception CTERM;
2007-04-03 ago avoid clash with Alice keywords;
2007-02-26 ago moved some non-kernel material to more_thm.ML;
2007-02-04 ago old-fashioned abstype ctyp/cterm/thm prevents accidental equality tests;
2007-01-02 ago Term.lambda: abstract over arbitrary closed terms;
2006-12-12 ago tuned error messages;
2006-12-05 ago thm/prf: separate official name vs. additional tags;
2006-11-29 ago simplified Logic.count_prems;
2006-11-21 ago moved theorem kinds from PureThy to Thm;
2006-11-05 ago removed obsolete first_duplicate;
2006-10-31 ago fixed type signature of Type.varify
2006-10-11 ago abandoned findrep
2006-10-07 ago added def_name_optional;
2006-10-01 ago cterm_match: avoid recalculation of maxidx;
2006-09-21 ago added dest_binop;
2006-09-18 ago added dest_arg, i.e. a tuned version of #2 o dest_comb;
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-09-15 ago instantiate: omit has_duplicates check, which is irrelevant for soundness;
2006-09-12 ago ctyp: maintain maxidx;
2006-08-08 ago abandoned equal_list in favor for eq_list
2006-08-03 ago tuned;
2006-08-02 ago normalized Proof.context/method type aliases;
2006-07-30 ago adjust_maxidx: pass explicit lower bound;
2006-07-11 ago replaced Term.variant(list) by Name.variant(_list);
2006-07-08 ago tuned exception handling;
2006-07-04 ago varifyT: no longer pervasive;
2006-06-17 ago added generalize rule;
2006-06-13 ago added hyps_of;
2006-06-12 ago tuned Seq/Envir/Unify interfaces;
2006-05-01 ago class_triv: Sign.certify_class;
2006-04-29 ago added unconstrainT;
2006-04-26 ago curried Seq.cons;
2006-04-13 ago added maxidx_of;
2006-03-21 ago avoid polymorphic equality;
2006-03-10 ago Shortened the exception messages from assume.
2006-02-11 ago tuned;
2006-02-07 ago removed obsolete sign_of_cterm;
2006-02-06 ago union_tpairs: Library.merge;
2006-01-21 ago simplified type attribute;
2005-12-23 ago turned bicompose_no_flatten into compose_no_flatten, without elimination;
2005-12-22 ago added bicompose_no_flatten, which refrains from
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-11-16 ago tuned Pattern.match/unify;
2005-11-10 ago renamed Thm.cgoal_of to Thm.cprem_of;
2005-11-09 ago Thm.varifyT': natural argument order;
2005-10-28 ago added cgoal_of;
2005-10-15 ago tuned comment;
2005-09-29 ago abstract_rule: tuned exception msgs;
2005-09-15 ago TableFun/Symtab: curried lookup and update;