1998-08-13 ago Rule mk_triv_goal for making instances of triv_goal
1998-06-25 ago added rewrite_cterm;
1998-04-04 ago added triv_goal, rev_triv_goal (for Isar);
1998-03-10 ago New simplifier flag for mutual simplification.
1998-03-09 ago Syntax.indexname;
1998-03-04 ago Reorganized simplifier. May now reorient rules.
1998-02-07 ago Tidying; rotate_prems; moved freeze_thaw from tactic.ML
1998-01-30 ago removed dead messy code;
1997-12-19 ago adapted to new sort function;
1997-11-27 ago removed same_thm;
1997-11-26 ago cleaned signature;
1997-11-24 ago Added read_def_cterms for simultaneous reading/typing of terms under
1997-11-21 ago changed Sequence interface (now Seq, in seq.ML);
1997-11-01 ago propagate exn msg;
1997-10-28 ago eq_thm moved to thm.ML;
1997-10-24 ago ProtoPure.thy;
1997-10-01 ago moved theory stuff (add_defs etc.) to theory.ML;
1997-09-02 ago Added Larry's equal_intr_rule
1997-07-25 ago improved rewrite_thm / rewrite_goals to handle conditional eqns;
1997-07-23 ago added rewrite_thm;
1997-07-18 ago defs: allow conditions;
1997-02-21 ago Replaced "flat" by the Basis Library function List.concat
1996-11-28 ago Replaced map...~~ by
1996-11-13 ago Removal of polymorphic equality via mem, subset, eq_set, etc
1996-11-01 ago Now uses Int.max instead of max
1996-09-23 ago New operations on cterms. Now same names as in Logic
1996-08-12 ago Improved (?) wording of error message
1996-05-22 ago Added swap_prems_rl
1996-04-30 ago moved dest_cimplies to drule.ML; added adjust_maxidx
1996-03-21 ago Printing & string functions moved to display.ML
1996-02-16 ago Elimination of fully-functorial style.
1996-01-29 ago inserted tabs again
1996-01-29 ago removed tabs
1996-01-15 ago improved printing of errors in 'defs';
1996-01-11 ago Removed bug in type unification. Negative indexes are not used any longer.
1995-12-22 ago Now "standard" compresses theorems (for sharing).
1995-09-01 ago added same_sg and same_thm
1995-09-01 ago adapted to new version of shyps-stuff;
1995-08-01 ago modified pretty_thm, standard, eq_thm to handle shyps;
1995-07-25 ago Added weak_eq_thm and forall_intr_vars (thanks to Mark Staples)
1995-03-14 ago Removed an old bug which made some simultaneous instantiations fail if they
1995-03-13 ago Changed treatment of during type inference internally generated type
1995-03-03 ago added CPure (curried functions) and ProtoPure (ancestor of Pure and CPure)
1995-01-11 ago removed print_sign, print_axioms;
1994-12-09 ago improved axioms_of: returns thms as the manual says;
1994-11-14 ago Pure/drule/cprems_of, cskip_flexpairs, cstrip_imp_prems: new cterm operations
1994-10-31 ago Pure/drule/thin_rl: new
1994-10-25 ago minor change of occs_const in dest_defn;
1994-10-12 ago add_defs: improved error messages;
1994-08-23 ago added print_syntax: theory -> unit;
1994-08-19 ago added add_defs, add_defs_i;
1994-05-26 ago replaced ext_axtab by new_axioms;
1994-05-19 ago added print_sign, print_axioms: theory -> unit;
1994-02-03 ago removed eq_sg, pprint_sg, print_sg (now in sign.ML);
1994-01-18 ago Pure: MAJOR CHANGE. Moved ML types ctyp and cterm and their associated
1994-01-05 ago added new parameter to the simplification tactics which indicates if
1994-01-04 ago added fake_cterm_of to speed up rewriting
1994-01-04 ago commented out sig constraint of functor (for debugging purposes);
1993-12-21 ago pretty_thm is now exported;
1993-10-21 ago Pure/drule/print_goals_ref: new, for Centaur interface