1997-06-04 wenzelm 1997-06-04 eliminated freeze_vars;
1997-04-16 wenzelm 1997-04-16 Sorts.str_of_arity;
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
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.
1995-09-01 wenzelm 1995-09-01 adapted to new version of shyps-stuff;
1995-08-01 wenzelm 1995-08-01 modified prep_thm_axm to handle shyps; fixed class_axms: class_trivs *first*; improved axclass_tac: now also handles object rules as witnesses;
1995-07-27 wenzelm 1995-07-27 minor fix: instance now raises error if witness axioms don't exist;
1995-01-27 wenzelm 1995-01-27 instance: now automatically includes defs of current thy node as witnesses;
1994-10-12 wenzelm 1994-10-12 prove_subclass, prove_arity now exported; minor internal changes;
1994-08-19 wenzelm 1994-08-19 cleaned sig; removed add_defns (now in drule.ML as add_defs); removed add_sigclass; minor internal changes;
1994-07-27 wenzelm 1994-07-27 added experimental add_defns (actually should be moved somewhere else); minor internal changes;
1994-07-14 wenzelm 1994-07-14 added functor signature constraint;
1994-07-06 wenzelm 1994-07-06 various minor changes (names and comments);
1994-06-16 wenzelm 1994-06-16 (beta release)
1994-05-26 wenzelm 1994-05-26 axiomatic type class 'package' for Pure (alpha version);