2006-12-28 ago tuned msg;
2006-12-27 ago fixed misleading error message
2006-12-21 ago code clarifications
2006-12-07 ago reorganized structure Goal vs. Tactic;
2006-11-22 ago completed class parameter handling in axclass.ML
2006-09-19 ago Logic.name_classrel/arities;
2006-09-15 ago renamed Term.map_term_types to Term.map_types (cf. Term.fold_types);
2006-07-30 ago Thm.adjust_maxidx;
2006-07-12 ago class_of_param instead of class_of
2006-07-08 ago Goal.prove: context;
2006-06-28 ago added lookup function for parameters
2006-05-24 ago axiomatize class: Theory.add_deps;
2006-05-20 ago class axiomatization: finals;
2006-05-16 ago more abstract interface to classes/arities;
2006-05-07 ago removed 'concl is' patterns;
2006-05-05 ago of_sort: explicit cache value;
2006-05-02 ago tuned;
2006-05-02 ago of_sort: option;
2006-05-01 ago of_sort: simplified derivation;
2006-04-30 ago renamed add_axclass(_i) to define_axclass(_i);
2006-04-29 ago instances data: mutable cache;
2006-04-27 ago tuned basic list operators (flat, maps, map_filter);
2006-04-25 ago get_info: removed 'super' field;
2006-04-13 ago reworded add_axclass(_i): canonical specification format,
2006-04-11 ago moved abstract syntax operations to logic.ML;
2006-04-10 ago fixed value restriction
2006-04-10 ago add_axclass(_i): return class name only;
2006-03-11 ago moved read_class, read/cert_classrel/arity to sign.ML;
2006-02-24 ago Reverted to old interface of AxClass.add_inst_arity(_i)
2006-02-22 ago renamed class_axms to class_intros;
2006-02-20 ago moved intro_classes from AxClass to ClassPackage
2006-02-07 ago renamed gen_duplicates to duplicates;
2006-02-06 ago Logic.const_of_class/class_of_const;
2006-01-30 ago moved instance Isar command to class_package.ML
2006-01-27 ago moved theorem tags from Drule to PureThy;
2006-01-23 ago exported after_qed for axclass instance
2006-01-21 ago simplified type attribute;
2006-01-19 ago setup: theory -> theory;
2006-01-14 ago sane ERROR handling;
2006-01-04 ago exported read|cert_arity interfaces
2005-12-22 ago Tactic.precise_conjunction_tac;
2005-12-16 ago re-arranged tuples (theory * 'a) to ('a * theory) in Pure
2005-12-09 ago oriented result pairs in PureThy
2005-11-08 ago simplified after_qed;
2005-10-21 ago Goal.prove;
2005-10-19 ago removed obsolete axclass_tac, add_inst_subclass_x, add_inst_arity_x;
2005-10-15 ago goal statements: accomodate before_qed argument;
2005-10-04 ago minor tweaks for Poplog/ML;
2005-09-29 ago Theory.add_finals_i;
2005-09-20 ago slight adaptions to library changes
2005-09-15 ago TableFun/Symtab: curried lookup and update;
2005-09-13 ago tuned Isar interfaces;
2005-09-06 ago name space prefix is now "c_class" instead of just "c";
2005-09-01 ago curried_lookup/update;
2005-08-16 ago OuterKeyword;
2005-08-09 ago exported after_qed for arity proofs
2005-08-08 ago After_qed takes result argument.
2005-06-20 ago get_thm(s): Name;
2005-06-17 ago accomodate change of TheoryDataFun;
2005-06-11 ago refer to name spaces values instead of names;