src/Pure/axclass.ML
2006-07-30 wenzelm 2006-07-30 Thm.adjust_maxidx;
2006-07-12 haftmann 2006-07-12 class_of_param instead of class_of
2006-07-08 wenzelm 2006-07-08 Goal.prove: context;
2006-06-28 haftmann 2006-06-28 added lookup function for parameters
2006-05-24 wenzelm 2006-05-24 axiomatize class: Theory.add_deps;
2006-05-20 wenzelm 2006-05-20 class axiomatization: finals;
2006-05-16 wenzelm 2006-05-16 more abstract interface to classes/arities;
2006-05-07 wenzelm 2006-05-07 removed 'concl is' patterns;
2006-05-05 wenzelm 2006-05-05 of_sort: explicit cache value; simplified internal representation of instances;
2006-05-02 wenzelm 2006-05-02 tuned;
2006-05-02 wenzelm 2006-05-02 of_sort: option; of_sort: simplified implementation, use Sorts.of_sort_derivation; tuned;
2006-05-01 wenzelm 2006-05-01 of_sort: simplified derivation;
2006-04-30 wenzelm 2006-04-30 renamed add_axclass(_i) to define_axclass(_i); renamed get_info to get_definition; added axiomatize_class/classrel/arity (supercede Sign.add_classes/classrel/arities); tuned;
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;