src/Pure/axclass.ML
2008-05-18 wenzelm 2008-05-18 moved global pretty/string_of functions from Sign to Syntax;
2008-04-02 haftmann 2008-04-02 removed obscure "attach" feature
2008-03-10 haftmann 2008-03-10 exported suffix
2008-01-08 haftmann 2008-01-08 better error reporting
2007-12-13 haftmann 2007-12-13 exported axiomsN
2007-12-11 haftmann 2007-12-11 error handling for pathological cases
2007-12-10 haftmann 2007-12-10 moved instance parameter management from class.ML to axclass.ML
2007-11-28 haftmann 2007-11-28 naming policy for instances
2007-10-11 wenzelm 2007-10-11 moved define_class_params to Isar/class.ML; removed obsolete params_of_class, print_axclasses; moved ProofContext.pp to Syntax.pp; misc tuning;
2007-10-09 wenzelm 2007-10-09 renamed AxClass.get_definition to AxClass.get_info (again); AxClass.axiomatize: renamed XXX_i to XXX, and XXX to XXX_cmd;
2007-10-09 wenzelm 2007-10-09 generic Syntax.pretty/string_of operations;
2007-10-04 wenzelm 2007-10-04 replaced AxClass.param_tyvarname by Name.aT;
2007-09-30 wenzelm 2007-09-30 Sign.add_consts_authentic: tags (Markup.property list);
2007-09-29 wenzelm 2007-09-29 Sign.add_const_constraint;
2007-09-26 wenzelm 2007-09-26 Sign.minimize/complete_sort;
2007-09-25 wenzelm 2007-09-25 proper Sign operations instead of Theory aliases;
2007-09-23 wenzelm 2007-09-23 tuned;
2007-09-15 haftmann 2007-09-15 clarified class interfaces and internals
2007-08-14 wenzelm 2007-08-14 avoid low-level tsig;
2007-06-19 wenzelm 2007-06-19 balanced conjunctions; added split_defined (from conjunction.ML);
2007-05-07 wenzelm 2007-05-07 simplified DataFun interfaces;
2007-04-20 haftmann 2007-04-20 moved axclass module closer to core system
2007-04-15 wenzelm 2007-04-15 Thm.fold_terms;
2007-04-03 wenzelm 2007-04-03 renamed of_sort_derivation record fields (avoid clash with Alice keywords);
2007-03-02 haftmann 2007-03-02 syntax for "class attach const"
2006-12-29 haftmann 2006-12-29 cleanup
2006-12-29 wenzelm 2006-12-29 replaced Sign.classes by Sign.all_classes (topologically sorted);
2006-12-29 haftmann 2006-12-29 dropped some bookkeeping
2006-12-28 wenzelm 2006-12-28 tuned msg;
2006-12-27 haftmann 2006-12-27 fixed misleading error message
2006-12-21 haftmann 2006-12-21 code clarifications
2006-12-07 wenzelm 2006-12-07 reorganized structure Goal vs. Tactic;
2006-11-22 haftmann 2006-11-22 completed class parameter handling in axclass.ML
2006-09-19 wenzelm 2006-09-19 Logic.name_classrel/arities;
2006-09-15 wenzelm 2006-09-15 renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
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;