src/Pure/drule.ML
2006-06-12 wenzelm 2006-06-12 tuned Seq/Envir/Unify interfaces;
2006-06-11 wenzelm 2006-06-11 outer_params: Syntax.dest_internal;
2006-06-05 wenzelm 2006-06-05 support embedded terms;
2006-06-01 paulson 2006-06-01 Tiny code cleanup
2006-05-26 wenzelm 2006-05-26 forall_intr_list: do not ignore errors;
2006-05-01 wenzelm 2006-05-01 added sort_triv;
2006-04-29 wenzelm 2006-04-29 added unconstrainTs;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-13 wenzelm 2006-04-13 added equal_elim_rule2; export dest_binop; export store_thm etc; moved conjunction stuff to conjunction.ML;
2006-03-04 wenzelm 2006-03-04 added mk_conjunction; tuned conj_curry;
2006-02-22 wenzelm 2006-02-22 removed rename_indexes_wrt; added rename_indexes2; simplified Pure conjunction, based on actual const;
2006-02-15 wenzelm 2006-02-15 added distinct_prems_rl;
2006-02-06 wenzelm 2006-02-06 Envir.(beta_)eta_contract;
2006-02-03 wenzelm 2006-02-03 removed add/del_rules;
2006-01-28 wenzelm 2006-01-28 added equals_cong;
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
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';