src/Pure/drule.ML
2006-01-25 wenzelm 2006-01-25 abs_def: improved error;
2006-01-21 wenzelm 2006-01-21 simplified type attribute; moved rule/declaration_attribute to thm.ML;
2006-01-10 wenzelm 2006-01-10 added declaration_attribute;
2005-12-31 wenzelm 2005-12-31 tuned forall_intr_vars;
2005-12-23 wenzelm 2005-12-23 conj_elim_precise: proper treatment of nested conjunctions;
2005-12-22 wenzelm 2005-12-22 fixed has_internal; added is_internal; renamed imp_cong' to imp_cong_rule; uniform versions of forall_conv, concl_conv, prems_conv, conjunction_conv;
2005-12-08 wenzelm 2005-12-08 removed Syntax.deskolem;
2005-12-02 wenzelm 2005-12-02 abs_def: beta/eta contract lhs;
2005-11-25 wenzelm 2005-11-25 forall_conv: limit prefix;
2005-11-22 wenzelm 2005-11-22 export map_tags; added multi_resolve(s) -- from Isar/method.ML;
2005-11-19 wenzelm 2005-11-19 removed conj_mono; added conj_curry; tuned;
2005-11-16 wenzelm 2005-11-16 added protect_cong, cong_mono_thm; outer_params: Syntax.deskolem;
2005-11-09 wenzelm 2005-11-09 added fold_terms; added tfrees_of, frees_of; tvars_intr_list: natural argument order;
2005-11-08 wenzelm 2005-11-08 removed impose_hyps, satisfy_hyps; tuned;
2005-10-28 wenzelm 2005-10-28 added incr_indexes; added lift_all (approx. reverse of gen_all); renamed Goal constant to prop, more general protect/unprotect interfaces;
2005-10-21 wenzelm 2005-10-21 renamed triv_goal to goalI, rev_triv_goal to goalD; removed mk_triv_goal (cf. Goal.init);
2005-09-29 berghofe 2005-09-29 Optimized and exported flexflex_unique.
2005-09-26 wenzelm 2005-09-26 moved disambiguate_frees to ProofKernel;
2005-09-26 obua 2005-09-26 added Drule.disambiguate_frees : thm -> thm
2005-09-12 haftmann 2005-09-12 introduced new-style AList operations
2005-08-31 wenzelm 2005-08-31 refer to theory instead of low-level tsig;
2005-08-01 wenzelm 2005-08-01 replaced atless by term_ord;
2005-07-28 wenzelm 2005-07-28 tuned gen_all, forall_elim_list, implies_intr_list, standard; impose_hyps: use Thm.weaken; zero_var_indexes: use Term.zero_var_indexes_inst; Sign.typ_unify;
2005-07-15 wenzelm 2005-07-15 tuned fold on terms;
2005-07-13 haftmann 2005-07-13 (fix for an accidental commit)
2005-07-13 haftmann 2005-07-13 (intermediate commit)
2005-07-06 wenzelm 2005-07-06 Thm.full_prop_of;
2005-07-04 wenzelm 2005-07-04 tuned;
2005-06-29 wenzelm 2005-06-29 added implies_intr_hyps (from thm.ML);
2005-06-17 wenzelm 2005-06-17 accomodate identification of type Sign.sg and theory;
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;