src/Pure/drule.ML
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.
1996-01-29 clasohm 1996-01-29 inserted tabs again
1996-01-29 clasohm 1996-01-29 removed tabs
1996-01-15 wenzelm 1996-01-15 improved printing of errors in 'defs'; fixed small bug in 'standard' (it used to fail stripping shyps in some cases);
1996-01-11 nipkow 1996-01-11 Removed bug in type unification. Negative indexes are not used any longer. Had to change interface to Type.unify to pass maxidx. Thus changes in the clients.
1995-12-22 paulson 1995-12-22 Now "standard" compresses theorems (for sharing). Also, rewrite_rule and rewrite_goals_rule check for the empty list of rewrites and do nothing in that case.
1995-09-01 clasohm 1995-09-01 added same_sg and same_thm
1995-09-01 wenzelm 1995-09-01 adapted to new version of shyps-stuff;
1995-08-01 wenzelm 1995-08-01 modified pretty_thm, standard, eq_thm to handle shyps;
1995-07-25 lcp 1995-07-25 Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
1995-03-14 nipkow 1995-03-14 Removed an old bug which made some simultaneous instantiations fail if they were given in the "wrong" order. Rewrote sign/infer_types. Fixed some comments.