src/Pure/drule.ML
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";
2000-11-07 berghofe 2000-11-07 - new theorems imp_cong and swap_prems_eq - new function dest_equals - exported strip_imp_concl - removed incr_indexes (now in Thm)
2000-11-06 wenzelm 2000-11-06 Sign.typ_instance;
2000-09-05 wenzelm 2000-09-05 improved add_rules;
2000-09-04 wenzelm 2000-09-04 added add_rules, del_rules;
2000-08-08 wenzelm 2000-08-08 added forall_elim_vars_safe, norm_hhf_eq;
2000-08-07 paulson 2000-08-07 more cterm operations: mk_implies, list_implies
2000-07-30 wenzelm 2000-07-30 Logic.goal_const;
2000-07-27 wenzelm 2000-07-27 export has_internal; tag some rules as internal;
2000-07-24 wenzelm 2000-07-24 Drule.merge_rules;
2000-07-12 wenzelm 2000-07-12 infix 'OF' is a version of 'MRS' with more appropriate argument order;
2000-03-30 wenzelm 2000-03-30 added tvars_intr_list;
2000-03-22 paulson 2000-03-22 new meta-rule "inst", a shorthand for read_instantiate_sg
2000-03-17 wenzelm 2000-03-17 untag: remove all tags of given name;
2000-03-10 berghofe 2000-03-10 Type.unify and Type.typ_match now use Vartab instead of association lists.
2000-03-08 wenzelm 2000-03-08 added (un)tag_rule;
2000-03-02 wenzelm 2000-03-02 added freeze_all; tuned spacing;
2000-01-17 paulson 2000-01-17 Thm.instantiate no longer normalizes, but Drule.instantiate does
2000-01-05 wenzelm 2000-01-05 TypeInfer.logicT;
1999-10-21 wenzelm 1999-10-21 forall_elim_var(s) moved to pure_thy.ML;
1999-09-29 wenzelm 1999-09-29 strip_shyps_warning;
1999-09-04 wenzelm 1999-09-04 handle Bind!!
1999-09-01 wenzelm 1999-09-01 PureThy.smart_store_thms;
1999-08-27 wenzelm 1999-08-27 thm "_" = asm_rl;
1999-08-18 paulson 1999-08-18 new primitive rule permute_prems to underlie defer_tac and rotate_prems
1999-07-13 wenzelm 1999-07-13 added mk_cgoal, assume_goal;
1999-07-09 wenzelm 1999-07-09 added compose_single;
1999-07-08 wenzelm 1999-07-08 improved error msgs of cterm_instantiate; fixed incr_indexes;
1999-04-16 wenzelm 1999-04-16 added incr_indexes, incr_indexes_wrt;
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1999-01-12 wenzelm 1999-01-12 added rule_attribute: ('a -> thm -> thm) -> 'a attribute; added tag / untag attributes;
1998-11-17 wenzelm 1998-11-17 export vars_of and friends; open BasicDrule only;
1998-10-20 wenzelm 1998-10-20 added unvarify(T);
1998-08-13 paulson 1998-08-13 Rule mk_triv_goal for making instances of triv_goal
1998-06-25 wenzelm 1998-06-25 added rewrite_cterm;
1998-04-04 wenzelm 1998-04-04 added triv_goal, rev_triv_goal (for Isar);
1998-03-10 nipkow 1998-03-10 New simplifier flag for mutual simplification.
1998-03-09 wenzelm 1998-03-09 Syntax.indexname;