2000-11-18 ago default_intro_classes_tac: Tactic.distinct_subgoals_tac;
2000-11-13 ago tuned IsarThy.theorem_i;
2000-10-23 ago intro_classes by default;
2000-09-17 ago Display.pretty_thm_sg;
2000-05-23 ago eta-expanded to handle value polymorphism
2000-05-21 ago adapted to inner syntax of sorts;
2000-04-17 ago Pretty.chunks;
2000-04-14 ago intrn_arity: reject type abbreviations;
2000-04-05 ago HEADGOAL;
2000-03-18 ago intro_classes_tac: REPEAT_ALL_NEW;
2000-03-13 ago adapted to new PureThy.add_thms etc.;
1999-08-25 ago expand_classes renamed to intro_classes;
1999-07-08 ago propp: 'concl' patterns;
1999-05-25 ago formal comments (still dummy);
1999-05-24 ago outer syntax keyword classification;
1999-05-21 ago improved errors;
1999-04-30 ago theory data: copy;
1999-03-17 ago qualify Theory.sign_of etc.;
1999-03-17 ago theory data;
1999-01-12 ago eliminated Attribute structure;
1998-10-20 ago quiet_mode, message;
1998-05-15 ago witnesses: lookup stored thms instead of axioms;
1998-05-13 ago tuned msg;
1998-04-29 ago adapted to new PureThy.add_axioms_i;
1997-10-28 ago add_store_axioms_i;
1997-10-24 ago removed add_thms_as_axms;
1997-10-20 ago tuned types;
1997-10-20 ago fixed goal_XXX;
1997-10-20 ago fixed types of add_XXX;
1997-10-13 ago uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
1997-10-09 ago fixed axiom names;
1997-10-06 ago eliminated raise_term, raise_typ;
1997-10-01 ago fully qualified names: Theory.add_XXX;
1997-08-06 ago added "Proving ..." msgs;
1997-06-04 ago eliminated freeze_vars;
1997-04-16 ago Sorts.str_of_arity;
1997-02-21 ago Replaced "flat" by the Basis Library function List.concat
1996-11-28 ago Replaced map...~~ by
1996-02-16 ago Elimination of fully-functorial style.
1995-09-01 ago adapted to new version of shyps-stuff;
1995-08-01 ago modified prep_thm_axm to handle shyps;
1995-07-27 ago minor fix: instance now raises error if witness axioms don't exist;
1995-01-27 ago instance: now automatically includes defs of current thy node as witnesses;
1994-10-12 ago prove_subclass, prove_arity now exported;
1994-08-19 ago cleaned sig;
1994-07-27 ago added experimental add_defns (actually should be moved somewhere else);
1994-07-14 ago added functor signature constraint;
1994-07-06 ago various minor changes (names and comments);
1994-06-16 ago (beta release)
1994-05-26 ago axiomatic type class 'package' for Pure (alpha version);