src/Pure/drule.ML
2005-05-10 paulson 2005-05-10 new cterm primitives
2005-05-04 berghofe 2005-05-04 Added eta_long_conversion.
2005-04-28 wenzelm 2005-04-28 added plain_prop_of;
2005-04-21 berghofe 2005-04-21 - Eliminated nodup_vars check. - Unification and matching functions now check types of term variables / sorts of type variables when applying a substitution. - Thm.instantiate now takes (ctyp * ctyp) list instead of (indexname * ctyp) list as argument, to allow for proper instantiation of theorems containing type variables with same name but different sorts.
2005-04-07 wenzelm 2005-04-07 added add_used; include tpairs;
2005-03-04 skalberg 2005-03-04 Removed practically all references to Library.foldr.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-22 dixon 2005-02-22 Lucas - fixed bug in zero_var_indexes: it was ignoring vars in the flex-flex pairs. These are now taken into account.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-02-03 paulson 2005-02-03 new treatment of demodulation in proof reconstruction
2005-01-18 berghofe 2005-01-18 Added variants of instantiation functions that operate on pairs of type (indexname * string) instead of (string * string).
2004-10-26 berghofe 2004-10-26 Added function strip_type (for ctyps).
2004-06-23 skalberg 2004-06-23 Moved conversion rules from MetaSimplifier to Drule. refl_implies removed from Drule, instead imp_cong' exported from there.
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-29 wenzelm 2004-05-29 improved output;
2004-04-22 wenzelm 2004-04-22 tuned;
2004-02-19 paulson 2004-02-19 comments!!
2004-02-17 berghofe 2004-02-17 Moved application of flexflex_unique from standard' to standard.
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";