2009-03-12 ago renamed sticky_prefix to mandatory_path;
2009-03-12 ago replaced old-style add_path/no_base_names by sticky_prefix;
2009-03-08 ago moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 ago more uniform handling of binding in targets and derived elements;
2009-03-05 ago renamed NameSpace.base to NameSpace.base_name;
2009-03-04 ago merged
2009-03-04 ago explicit error message for `improper` instances lacking explicit instance parameter constants
2009-03-03 ago Thm.binding;
2009-01-21 ago binding replaces bstring
2009-01-17 ago close derivation of classrels
2008-12-04 ago cleaned up binding module and related code
2008-09-03 ago Sign.declare_const: Name.binding;
2008-09-02 ago explicit type Name.binding for higher-specification elements;
2008-08-27 ago completing arities after subclass instance
2008-08-14 ago moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-07-29 ago PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-25 ago dropped PureThy.note; added PureThy.add_thm
2008-07-11 ago Sorts.weaken: abstract argument;
2008-07-11 ago explicit completions of arities
2008-07-08 ago refined arity property concept
2008-06-30 ago tagged arities
2008-05-18 ago moved global pretty/string_of functions from Sign to Syntax;
2008-04-02 ago removed obscure "attach" feature
2008-03-10 ago exported suffix
2008-01-08 ago better error reporting
2007-12-13 ago exported axiomsN
2007-12-11 ago error handling for pathological cases
2007-12-10 ago moved instance parameter management from class.ML to axclass.ML
2007-11-28 ago naming policy for instances
2007-10-11 ago moved define_class_params to Isar/class.ML;
2007-10-09 ago renamed AxClass.get_definition to AxClass.get_info (again);
2007-10-09 ago generic Syntax.pretty/string_of operations;
2007-10-04 ago replaced AxClass.param_tyvarname by Name.aT;
2007-09-30 ago Sign.add_consts_authentic: tags ( list);
2007-09-29 ago Sign.add_const_constraint;
2007-09-26 ago Sign.minimize/complete_sort;
2007-09-25 ago proper Sign operations instead of Theory aliases;
2007-09-23 ago tuned;
2007-09-15 ago clarified class interfaces and internals
2007-08-14 ago avoid low-level tsig;
2007-06-19 ago balanced conjunctions;
2007-05-07 ago simplified DataFun interfaces;
2007-04-20 ago moved axclass module closer to core system
2007-04-15 ago Thm.fold_terms;
2007-04-03 ago renamed of_sort_derivation record fields (avoid clash with Alice keywords);
2007-03-02 ago syntax for "class attach const"
2006-12-29 ago cleanup
2006-12-29 ago replaced Sign.classes by Sign.all_classes (topologically sorted);
2006-12-29 ago dropped some bookkeeping
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