src/Pure/axclass.ML
2001-10-27 wenzelm 2001-10-27 removed obsolete goal_subclass, goal_arity;
2001-10-18 wenzelm 2001-10-18 sane internal interfaces for instance;
2001-10-13 wenzelm 2001-10-13 IsarThy.theorem_i Drule.internalK;
2001-08-31 wenzelm 2001-08-31 proper use of invent_names;
2001-08-31 wenzelm 2001-08-31 tuned headers;
2001-05-31 wenzelm 2001-05-31 invent_names
2001-02-12 wenzelm 2001-02-12 support \<subseteq> syntax in classes/classrel/axclass/instance;
2000-11-21 wenzelm 2000-11-21 Tactic.distinct_subgoals_tac moved to internal intro_classes_tac;
2000-11-18 wenzelm 2000-11-18 default_intro_classes_tac: Tactic.distinct_subgoals_tac;
2000-11-13 wenzelm 2000-11-13 tuned IsarThy.theorem_i;
2000-10-23 wenzelm 2000-10-23 intro_classes by default;
2000-09-17 wenzelm 2000-09-17 Display.pretty_thm_sg;
2000-05-23 paulson 2000-05-23 eta-expanded to handle value polymorphism
2000-05-21 wenzelm 2000-05-21 adapted to inner syntax of sorts;
2000-04-17 wenzelm 2000-04-17 Pretty.chunks;
2000-04-14 wenzelm 2000-04-14 intrn_arity: reject type abbreviations;
2000-04-05 wenzelm 2000-04-05 HEADGOAL;
2000-03-18 wenzelm 2000-03-18 intro_classes_tac: REPEAT_ALL_NEW;
2000-03-13 wenzelm 2000-03-13 adapted to new PureThy.add_thms etc.;
1999-08-25 wenzelm 1999-08-25 expand_classes renamed to intro_classes;
1999-07-08 wenzelm 1999-07-08 propp: 'concl' patterns;
1999-05-25 wenzelm 1999-05-25 formal comments (still dummy);
1999-05-24 wenzelm 1999-05-24 outer syntax keyword classification; no open OuterParse;
1999-05-21 wenzelm 1999-05-21 improved errors;
1999-04-30 wenzelm 1999-04-30 theory data: copy;
1999-03-17 wenzelm 1999-03-17 qualify Theory.sign_of etc.;
1999-03-17 wenzelm 1999-03-17 theory data; attributes for class axioms; instance_subclass/arity_proof(_i); expand_classes proof method; 'axclass' / 'instance' outer syntax;
1999-01-12 wenzelm 1999-01-12 eliminated Attribute structure;
1998-10-20 wenzelm 1998-10-20 quiet_mode, message;
1998-05-15 wenzelm 1998-05-15 witnesses: lookup stored thms instead of axioms;
1998-05-13 wenzelm 1998-05-13 tuned msg;
1998-04-29 wenzelm 1998-04-29 adapted to new PureThy.add_axioms_i;
1997-10-28 wenzelm 1997-10-28 add_store_axioms_i;
1997-10-24 wenzelm 1997-10-24 removed add_thms_as_axms;
1997-10-20 wenzelm 1997-10-20 tuned types;
1997-10-20 wenzelm 1997-10-20 fixed goal_XXX;
1997-10-20 wenzelm 1997-10-20 fixed types of add_XXX; tuned;
1997-10-13 wenzelm 1997-10-13 uses Sign.str_of_classrel, Sign.str_of_arity, Sign.str_of_arity;
1997-10-09 wenzelm 1997-10-09 fixed axiom names;
1997-10-06 wenzelm 1997-10-06 eliminated raise_term, raise_typ; new internal forms: add_inst_subclass_i, add_inst_arity_i;
1997-10-01 wenzelm 1997-10-01 fully qualified names: Theory.add_XXX;
1997-08-06 wenzelm 1997-08-06 added "Proving ..." msgs;
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 ListPair.map
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);