2005-08-18 ago optimization to incr_indexes?
2005-07-19 ago incr_tvar (from term.ML), incr_indexes: avoid garbage;
2005-07-15 ago tuned;
2005-07-14 ago occs no longer infix (structure not open);
2005-05-31 ago added nth_prem;
2005-03-09 ago First version of global registration command.
2005-01-24 ago thin_tac now works on P==>Q
2005-01-21 ago fixed thin_tac with higher-level assumptions by removing the old code to
2003-07-31 ago Removed extraneous rev in function goal_params (the list of parameters
2003-07-11 ago Exported function goal_params.
2003-02-03 ago Moved get_goal, prems_of_goal and concl_of_goal from goals.ML to logic.ML
2002-10-21 ago Removed obsolete functions dealing with flex-flex constraints.
2002-02-20 ago Symbol.bump_string;
2002-01-17 ago is_norm_hhf moved to drule.ML;
2002-01-15 ago added mk_conjunction_list;
2001-11-11 ago added mk_conjunction;
2001-01-07 ago added is_norm_hhf;
2000-11-10 ago has_meta_prems: include "==";
2000-08-24 ago fixed strip_assums and assum_pairs, restoring them (essentially) to their
2000-08-21 ago fixed has_meta_prems: strip_assums_hyp;
2000-08-01 ago added has_meta_prems;
2000-07-30 ago Logic.goal_const;
1998-06-17 ago Goals may now contain assumptions, which are not returned.
1998-04-22 ago added mk_cond_defpair, mk_defpair;
1998-03-09 ago adapted to baroque chars;
1998-03-04 ago Reorganized simplifier. May now reorient rules.
1998-02-28 ago Tried to reorganize rewriter a little. More to be done.
1998-02-18 ago Improved loop-test for rewrite rules a little.
1997-12-19 ago term order stuff moved to term.ML;
1997-12-02 ago tuned term order;
1997-11-28 ago Fixed the definition of `termord': is now antisymmetric.
1997-11-04 ago logic: loops -> rewrite_rule_ok
1997-10-21 ago Corrected alphabetical order of entries in signature.
1997-10-17 ago Added "op" before "occs" to make sml/nj happy
1997-10-16 ago The simplifier has been improved a little: equations s=t which used to be
1997-06-05 ago Removal of freeze_vars and thaw_vars (quite unused...)
1997-01-16 ago added term order;
1996-11-28 ago Replaced map...~~ by
1996-06-28 ago Restored warning comment
1996-02-16 ago Elimination of fully-functorial style.
1996-01-29 ago inserted tabs again
1996-01-29 ago removed tabs
1994-10-12 ago added is_equals: term -> bool;
1994-09-06 ago Pure/type/unvarifyT: moved there from logic.ML
1994-08-18 ago /unvarifyT, unvarify: moved to Pure/logic.ML
1994-07-06 ago changed comment only;
1994-05-26 ago added mk_type, dest_type, mk_inclass, dest_inclass (for axclasses);
1994-01-04 ago commented out sig constraint of functor (for debugging purposes);
1993-10-21 ago logic/mk_equals,mk_flexpair: now calls fastype_of instead of type_of.
1993-09-16 ago Initial revision