src/Pure/drule.ML
2006-11-28 wenzelm 2006-11-28 dest_term: strip_imp_concl;
2006-11-24 wenzelm 2006-11-24 added cterm_rule;
2006-11-21 wenzelm 2006-11-21 moved theorem kinds from PureThy to Thm;
2006-10-09 wenzelm 2006-10-09 added dest_equals_lhs; replaced clhs/crhs_of by lhs/rhs_of; local_standard: flexflex_unique; removed strip_shyps_warning;
2006-10-07 wenzelm 2006-10-07 added term_rule;
2006-10-05 paulson 2006-10-05 a few new functions on thms and cterms
2006-09-21 wenzelm 2006-09-21 added dest_equals_rhs; moved dest_binop to thm.ML;
2006-09-18 wenzelm 2006-09-18 Thm.dest_arg;
2006-09-12 wenzelm 2006-09-12 moved term subst functions to TermSubst;
2006-08-03 wenzelm 2006-08-03 tuned types_sorts, add_used;
2006-08-02 wenzelm 2006-08-02 removed obsolete frees/vars_of etc.; removed obsolete freeze_all etc.; added norm_hhf_cterm; tuned fold_terms; renamed Syntax.indexname to Syntax.read_indexname;
2006-07-30 wenzelm 2006-07-30 Thm.adjust_maxidx;
2006-07-27 wenzelm 2006-07-27 removed obsolete equal_abs_elim(_list);
2006-07-11 wenzelm 2006-07-11 replaced Term.variant(list) by Name.variant(_list); Name.clean;
2006-07-04 wenzelm 2006-07-04 added generalize; removed obsolete assume_ax, tvars_intr_list;
2006-06-17 wenzelm 2006-06-17 Term.internal;
2006-06-13 wenzelm 2006-06-13 removed weak_eq_thm; added equiv_thm; removed obsolete unvarifyT; improved unvarify -- demands global context (cf. Logic.unvarify);
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;