src/Pure/axclass.ML
2006-04-29 wenzelm 2006-04-29 instances data: mutable cache; added of_sort: interface for derived instances;
2006-04-27 wenzelm 2006-04-27 tuned basic list operators (flat, maps, map_filter);
2006-04-25 wenzelm 2006-04-25 get_info: removed 'super' field; added params_of, all_params_of; removed params_of_sort; tuned;
2006-04-13 wenzelm 2006-04-13 reworded add_axclass(_i): canonical specification format, purely definitional version, always qualify intro/axioms;
2006-04-11 wenzelm 2006-04-11 moved abstract syntax operations to logic.ML; maintain class parameters; added params_of_sort; added cert/read_classrel (from sign.ML), check class parameters; tuned;
2006-04-10 haftmann 2006-04-10 fixed value restriction
2006-04-10 wenzelm 2006-04-10 add_axclass(_i): return class name only; subclass/arity statements: require actual TVars, store raw data; tuned;
2006-03-11 wenzelm 2006-03-11 moved read_class, read/cert_classrel/arity to sign.ML; axclass: moved outer syntax to isar_syn.ML; instance: moved to Tools/class_package.ML; simplified interfaces; tuned;
2006-02-24 berghofe 2006-02-24 Reverted to old interface of AxClass.add_inst_arity(_i)
2006-02-22 wenzelm 2006-02-22 renamed class_axms to class_intros;
2006-02-20 haftmann 2006-02-20 moved intro_classes from AxClass to ClassPackage
2006-02-07 wenzelm 2006-02-07 renamed gen_duplicates to duplicates;
2006-02-06 wenzelm 2006-02-06 Logic.const_of_class/class_of_const;
2006-01-30 haftmann 2006-01-30 moved instance Isar command to class_package.ML
2006-01-27 wenzelm 2006-01-27 moved theorem tags from Drule to PureThy;
2006-01-23 haftmann 2006-01-23 exported after_qed for axclass instance
2006-01-21 wenzelm 2006-01-21 simplified type attribute;
2006-01-19 wenzelm 2006-01-19 setup: theory -> theory;
2006-01-14 wenzelm 2006-01-14 sane ERROR handling;
2006-01-04 haftmann 2006-01-04 exported read|cert_arity interfaces
2005-12-22 wenzelm 2005-12-22 Tactic.precise_conjunction_tac;
2005-12-16 haftmann 2005-12-16 re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 haftmann 2005-12-09 oriented result pairs in PureThy
2005-11-08 wenzelm 2005-11-08 simplified after_qed;
2005-10-21 wenzelm 2005-10-21 Goal.prove;
2005-10-19 wenzelm 2005-10-19 removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
2005-10-15 wenzelm 2005-10-15 goal statements: accomodate before_qed argument;
2005-10-04 wenzelm 2005-10-04 minor tweaks for Poplog/ML;
2005-09-29 wenzelm 2005-09-29 Theory.add_finals_i;
2005-09-20 haftmann 2005-09-20 slight adaptions to library changes
2005-09-15 wenzelm 2005-09-15 TableFun/Symtab: curried lookup and update;
2005-09-13 wenzelm 2005-09-13 tuned Isar interfaces; tuned IsarThy.theorem_i;
2005-09-06 wenzelm 2005-09-06 name space prefix is now "c_class" instead of just "c"; export get_info; tuned;
2005-09-01 wenzelm 2005-09-01 curried_lookup/update;
2005-08-16 wenzelm 2005-08-16 OuterKeyword;
2005-08-09 haftmann 2005-08-09 exported after_qed for arity proofs
2005-08-08 ballarin 2005-08-08 After_qed takes result argument.
2005-06-20 wenzelm 2005-06-20 get_thm(s): Name;
2005-06-17 wenzelm 2005-06-17 accomodate change of TheoryDataFun; accomodate identification of type Sign.sg and theory;
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;