src/Pure/drule.ML
2004-02-15 paulson 2004-02-15 Polymorphic treatment of binary arithmetic using axclasses
2004-01-06 paulson 2004-01-06 correction to cterm_instantiate by Christoph Leuth
2003-06-29 berghofe 2003-06-29 Added functions for renaming bound variables.
2002-10-21 berghofe 2002-10-21 Removed obsolete functions dealing with flex-flex constraints.
2002-10-17 paulson 2002-10-17 fixing the cut_tac method to work when there are no instantiations and the supplied theorems have premises
2002-09-30 berghofe 2002-09-30 Removed nRS again because extract_rews now takes care of preserving names.
2002-09-19 nipkow 2002-09-19 drule: added nRS simplifier: trace with names
2002-07-18 wenzelm 2002-07-18 added satisfy_hyps;
2002-07-16 wenzelm 2002-07-16 added equal_elim_rule1;
2002-07-09 berghofe 2002-07-09 Added function abs_def.
2002-05-31 berghofe 2002-05-31 Changed interface of Pattern.rewrite_term.
2002-05-07 wenzelm 2002-05-07 use eq_thm_prop instead of slightly inadequate eq_thm;
2002-02-20 berghofe 2002-02-20 New function strip_comb (cterm version of Term.strip_comb).
2002-01-17 wenzelm 2002-01-17 added is_norm_hhf (from logic.ML); norm_hhf based on fast Pattern.rewrite_term;
2002-01-15 wenzelm 2002-01-15 conj_intr_list and conj_elim_precise: cover 0 conjuncts;
2002-01-12 wenzelm 2002-01-12 renamed forall_elim_vars_safe to gen_all;
2002-01-11 wenzelm 2002-01-11 improved forall_elim_vars_safe (no longer invents new indexes);
2002-01-11 wenzelm 2002-01-11 kind: ignore "";
2001-12-18 wenzelm 2001-12-18 tuned Type.unify;
2001-12-14 wenzelm 2001-12-14 export add_tvarsT etc.;
2001-12-05 wenzelm 2001-12-05 added add_rule, del_rule;
2001-11-26 wenzelm 2001-11-26 added remdups_rl;
2001-11-24 wenzelm 2001-11-24 gen_merge_lists';
2001-11-16 wenzelm 2001-11-16 local_standard: plain strip_shyps instead of strip_shyps_warning;
2001-11-11 wenzelm 2001-11-11 added conj_elim_precise, conj_intr_thm;
2001-11-09 berghofe 2001-11-09 Theorems symmetric, reflexive and transitive are now stored with "open" derivations.
2001-11-07 wenzelm 2001-11-07 tuned impose_hyps;
2001-11-05 wenzelm 2001-11-05 export add_tvarsT, add_tvars, add_vars, add_frees (would actually belong to term.ML, but is apt to cause some confusion with the fold-right versions there);
2001-10-31 wenzelm 2001-10-31 added local_standard;
2001-10-31 berghofe 2001-10-31 norm_hhf_eq is now stored using open_store_standard_thm.
2001-10-28 wenzelm 2001-10-28 rules for meta-level conjunction;
2001-10-27 wenzelm 2001-10-27 added impose_hyps;
2001-10-16 wenzelm 2001-10-16 added implies_intr_goals;
2001-10-13 wenzelm 2001-10-13 generic theorem kinds ("theorem", "lemma" etc.);
2001-08-31 berghofe 2001-08-31 Some basic rules are now stored with "open" derivations, to facilitate simplification of proof terms.
2001-02-20 oheimb 2001-02-20 added rearrange_prems
2001-02-14 berghofe 2001-02-14 imp_cong2 -> imp_cong
2001-01-07 wenzelm 2001-01-07 removed outdated comment;
2001-01-03 wenzelm 2001-01-03 Thm: dest_comb, dest_abs, capply, cabs no longer global;
2000-12-13 wenzelm 2000-12-13 eliminated GOAL syntax;
2000-11-23 wenzelm 2000-11-23 standard: close_derivation;
2000-11-10 wenzelm 2000-11-10 store_standard_thm "norm_hhf_eq";
2000-11-07 berghofe 2000-11-07 - new theorems imp_cong and swap_prems_eq - new function dest_equals - exported strip_imp_concl - removed incr_indexes (now in Thm)
2000-11-06 wenzelm 2000-11-06 Sign.typ_instance;
2000-09-05 wenzelm 2000-09-05 improved add_rules;
2000-09-04 wenzelm 2000-09-04 added add_rules, del_rules;
2000-08-08 wenzelm 2000-08-08 added forall_elim_vars_safe, norm_hhf_eq;
2000-08-07 paulson 2000-08-07 more cterm operations: mk_implies, list_implies
2000-07-30 wenzelm 2000-07-30 Logic.goal_const;
2000-07-27 wenzelm 2000-07-27 export has_internal; tag some rules as internal;
2000-07-24 wenzelm 2000-07-24 Drule.merge_rules;
2000-07-12 wenzelm 2000-07-12 infix 'OF' is a version of 'MRS' with more appropriate argument order;
2000-03-30 wenzelm 2000-03-30 added tvars_intr_list;
2000-03-22 paulson 2000-03-22 new meta-rule "inst", a shorthand for read_instantiate_sg
2000-03-17 wenzelm 2000-03-17 untag: remove all tags of given name;
2000-03-10 berghofe 2000-03-10 Type.unify and Type.typ_match now use Vartab instead of association lists.
2000-03-08 wenzelm 2000-03-08 added (un)tag_rule;
2000-03-02 wenzelm 2000-03-02 added freeze_all; tuned spacing;
2000-01-17 paulson 2000-01-17 Thm.instantiate no longer normalizes, but Drule.instantiate does
2000-01-05 wenzelm 2000-01-05 TypeInfer.logicT;