src/Pure/axclass.ML
2005-06-11 wenzelm 2005-06-11 refer to name spaces values instead of names;
2005-06-09 wenzelm 2005-06-09 got rid of bclass, xclass;
2005-06-02 wenzelm 2005-06-02 Theory.restore_naming;
2005-05-31 wenzelm 2005-05-31 renamed cond_extern to extern;
2005-05-17 wenzelm 2005-05-17 tuned;
2005-04-28 wenzelm 2005-04-28 sane interfaces for tactical instance proofs (do not expand defs of theory, proper handling of sort instances); keep legacy stuff separate; tuned;
2005-04-26 wenzelm 2005-04-26 export intro_classes_tac;
2005-04-21 wenzelm 2005-04-21 superceded by Pure.thy and CPure.thy;
2005-04-13 wenzelm 2005-04-13 *** MESSAGE REFERS TO PREVIOUS VERSION *** Attrib.src;
2005-04-13 wenzelm 2005-04-13 *** empty log message ***
2005-04-11 ballarin 2005-04-11 First release of interpretation commands.
2005-03-09 ballarin 2005-03-09 First version of global registration command.
2005-03-03 skalberg 2005-03-03 Move towards standard functions.
2005-02-13 skalberg 2005-02-13 Deleted Library.option type.
2005-01-24 berghofe 2005-01-24 Adapted to modified interface of PureThy.get_thm(s).
2004-06-21 kleing 2004-06-21 Merged in license change from Isabelle2004
2004-06-01 wenzelm 2004-06-01 removed obsolete sort 'logic';
2004-05-29 wenzelm 2004-05-29 improved output;
2004-05-21 wenzelm 2004-05-21 test_classrel/arity improve error reporting; tuned;
2004-05-01 wenzelm 2004-05-01 improved Term.invent_names;
2004-04-16 wenzelm 2004-04-16 'instance' and intro_classes now handle general sorts;
2002-02-12 wenzelm 2002-02-12 got rid of explicit marginal comments (now stripped earlier from input);
2002-01-10 wenzelm 2002-01-10 simplified IsarThy.theorem_i;
2001-12-14 wenzelm 2001-12-14 Term.invent_type_names;
2001-12-05 wenzelm 2001-12-05 tuned;
2001-11-28 wenzelm 2001-11-28 theory data: removed obsolete finish method;
2001-11-09 wenzelm 2001-11-09 theory data: finish method;
2001-11-04 wenzelm 2001-11-04 IsarThy.theorem_i (None, []);
2001-10-31 wenzelm 2001-10-31 IsarThy.theorem_i: no locale;
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;