2006-01-19 ago setup: theory -> theory;
2006-01-16 ago case_result: drop_schematic, i.e. be permissive about illegal binds;
2006-01-14 ago sane ERROR handling;
2006-01-13 ago uniform handling of fixes: read/cert_vars, add_fixes(_i), body flag;
2006-01-07 ago added infer_type, declared_type;
2006-01-07 ago support nested cases;
2005-12-22 ago cases: main is_proper flag;
2005-12-17 ago sort_distinct;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-08 ago removed Syntax.deskolem;
2005-12-02 ago removed fixed_tr: now handled in syntax module;
2005-11-30 ago match_bind(_i): return terms;
2005-11-25 ago revert_skolem: fall back on Syntax.deskolem;
2005-11-19 ago Goal.norm_hhf_protected;
2005-11-16 ago added revert_skolem, mk_def, add_def;
2005-11-10 ago moved find_free to term.ML;
2005-11-09 ago tvars_intr_list: natural argument order;
2005-11-08 ago removed export_plain;
2005-10-28 ago lthms_containing: not o valid_thms;
2005-10-28 ago added fact_tac, some_fact_tac;
2005-10-21 ago Goal.norm_hhf_rule;
2005-10-15 ago note_thmss, read/cert_vars etc.: natural argument order;
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-20 ago slight adaptions to library changes
2005-09-17 ago added auto_fix (from proof.ML);
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-14 ago tuned;
2005-09-13 ago added add_view, export_view (supercedes adhoc view arguments);
2005-09-01 ago curried_lookup/update;
2005-08-29 ago use AList operations;
2005-08-16 ago added transfer;
2005-08-01 ago Thm.full_prop_of;
2005-07-28 ago Sign.typ_unify;
2005-07-19 ago Inttab.defined;
2005-07-15 ago tuned fold on terms;
2005-07-14 ago sys_error;
2005-07-13 ago (fix for an accidental commit)
2005-07-13 ago (intermediate commit)
2005-07-01 ago avoid polyeq;
2005-06-22 ago removed proof data (see Pure/context.ML);
2005-06-20 ago thmref: Name vs. NameSelection;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-09 ago renamed extern to extern_thm;
2005-05-31 ago renamed cond_extern to extern;
2005-05-22 ago moved everything related to thms_containing to find_theorems.ML;
2005-05-17 ago tuned;
2005-05-17 ago moved credit to CONTRIBUTORS;
2005-05-17 ago use Drule.vars_of_terms
2005-05-16 ago searching for thms by combination of criteria (intro, elim, dest, name, term pattern)
2005-04-29 ago credits
2005-04-29 ago new thms_containing that searches for patterns instead of constants
2005-04-21 ago superceded by Pure.thy and CPure.thy;
2005-04-21 ago Adapted to new interface of instantiation and unification / matching functions.
2005-04-17 ago binds/thms: do not store options, but delete from table;
2005-04-16 ago Syntax.mk_trfun;
2005-04-15 ago Removed most of the atp interface from Pure.
2005-04-13 ago *** empty log message ***
2005-04-11 ago First release of interpretation commands.
2005-03-24 ago Further work on interpretation commands. New command `interpret' for