src/Pure/drule.ML
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;
1998-03-04 nipkow 1998-03-04 Reorganized simplifier. May now reorient rules. Moved loop tests from logic to thm.
1998-02-07 paulson 1998-02-07 Tidying; rotate_prems; moved freeze_thaw from tactic.ML
1998-01-30 wenzelm 1998-01-30 removed dead messy code;
1997-12-19 wenzelm 1997-12-19 adapted to new sort function;
1997-11-27 wenzelm 1997-11-27 removed same_thm;
1997-11-26 wenzelm 1997-11-26 cleaned signature; added instantiate': ctyp option list -> cterm option list -> thm -> thm;
1997-11-24 nipkow 1997-11-24 Added read_def_cterms for simultaneous reading/typing of terms under defaults. Redefined read_def_cterm in in terms of read_def_cterms. Deleted obsolete read_cterms. Cleaned up def of read_insts, which is not much shorter but much clearere are correcter now.
1997-11-21 wenzelm 1997-11-21 changed Sequence interface (now Seq, in seq.ML);
1997-11-01 wenzelm 1997-11-01 propagate exn msg;
1997-10-28 wenzelm 1997-10-28 eq_thm moved to thm.ML; store ProtoPure lemmas;
1997-10-24 wenzelm 1997-10-24 ProtoPure.thy;
1997-10-01 wenzelm 1997-10-01 moved theory stuff (add_defs etc.) to theory.ML;
1997-09-02 nipkow 1997-09-02 Added Larry's equal_intr_rule
1997-07-25 wenzelm 1997-07-25 improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-23 wenzelm 1997-07-23 added rewrite_thm;
1997-07-18 wenzelm 1997-07-18 defs: allow conditions;
1997-02-21 paulson 1997-02-21 Replaced "flat" by the Basis Library function List.concat
1996-11-28 paulson 1996-11-28 Replaced map...~~ by ListPair.map
1996-11-13 paulson 1996-11-13 Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-01 paulson 1996-11-01 Now uses Int.max instead of max
1996-09-23 paulson 1996-09-23 New operations on cterms. Now same names as in Logic
1996-08-12 paulson 1996-08-12 Improved (?) wording of error message
1996-05-22 nipkow 1996-05-22 Added swap_prems_rl
1996-04-30 clasohm 1996-04-30 moved dest_cimplies to drule.ML; added adjust_maxidx
1996-03-21 paulson 1996-03-21 Printing & string functions moved to display.ML
1996-02-16 paulson 1996-02-16 Elimination of fully-functorial style. Type tactic changed to a type abbrevation (from a datatype). Constructor tactic and function apply deleted.