src/Pure/drule.ML
2007-10-04 wenzelm 2007-10-04 replaced literal 'a by Name.aT;
2007-08-24 paulson 2007-08-24 new derived rule: incr_type_indexes
2007-08-13 wenzelm 2007-08-13 SimpleSyntax.read_prop;
2007-07-29 wenzelm 2007-07-29 moved Drule.add/del/merge_rules to Thm.add/del/merge_thms; moved Drule.is_dummy_thm to Thm.is_dummy;
2007-07-27 wenzelm 2007-07-27 added dummy_thm, is_dummy_thm;
2007-07-04 wenzelm 2007-07-04 added binop_cong_rule;
2007-07-03 wenzelm 2007-07-03 tuned rotate_prems; tuned comments;
2007-06-20 paulson 2007-06-20 A more robust flexflex_unique
2007-06-19 wenzelm 2007-06-19 added with_subgoal;
2007-05-31 wenzelm 2007-05-31 simplified/unified list fold;
2007-05-11 wenzelm 2007-05-11 proper type for fun/arg_cong_rule;
2007-05-11 wenzelm 2007-05-11 added fun/arg_cong_rule;
2007-05-10 wenzelm 2007-05-10 moved some operations to more_thm.ML and conv.ML;
2007-04-15 wenzelm 2007-04-15 moved Drule.plain_prop_of, Drule.fold_terms to more_thm.ML;
2007-04-14 wenzelm 2007-04-14 cleaned/simplified Sign.read_typ, Thm.read_cterm etc.; Term.string_of_vname;
2007-04-02 paulson 2007-04-02 optimizing the null instantiation case
2007-02-26 wenzelm 2007-02-26 moved eq_thm etc. to structure Thm in Pure/more_thm.ML;
2007-02-13 paulson 2007-02-13 COMP now performs a distinctness check on the multiple results before failing
2007-02-10 paulson 2007-02-10 Completing the bug fix from the previous update: the result of unifying type variables must be normalized WRT itself; otherwise instantiation is wrong
2007-02-08 paulson 2007-02-08 cterm_instantiate was calling a type instantiation function that works only for matching, not unification as here.
2007-01-19 wenzelm 2007-01-19 moved inst from drule.ML to old_goals.ML;
2006-12-05 wenzelm 2006-12-05 thm/prf: separate official name vs. additional tags;
2006-11-30 wenzelm 2006-11-30 added zero_var_indexes_list; removed local_standard (cf. Goal.norm/close_result); instantiate: more precise handling of indexes;
2006-11-29 wenzelm 2006-11-29 *** bad commit -- reverted to previous version ***
2006-11-29 wenzelm 2006-11-29 added INCR_COMP, COMP_INCR;
2006-11-29 wenzelm 2006-11-29 added INCR_COMP, COMP_INCR;
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;