2004-05-21 ago test_classrel/arity improve error reporting; tuned;
2004-05-01 ago improved Term.invent_names;
2004-04-16 ago 'instance' and intro_classes now handle general sorts;
2002-02-12 ago got rid of explicit marginal comments (now stripped earlier from input);
2002-01-10 ago simplified IsarThy.theorem_i;
2001-12-14 ago Term.invent_type_names;
2001-12-05 ago tuned;
2001-11-28 ago theory data: removed obsolete finish method;
2001-11-09 ago theory data: finish method;
2001-11-04 ago IsarThy.theorem_i (None, []);
2001-10-31 ago IsarThy.theorem_i: no locale;
2001-10-27 ago removed obsolete goal_subclass, goal_arity;
2001-10-18 ago sane internal interfaces for instance;
2001-10-13 ago IsarThy.theorem_i Drule.internalK;
2001-08-31 ago proper use of invent_names;
2001-08-31 ago tuned headers;
2001-05-31 ago invent_names
2001-02-12 ago support \<subseteq> syntax in classes/classrel/axclass/instance;
2000-11-21 ago Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
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;