src/Pure/axclass.ML
2009-09-30 wenzelm 2009-09-30 removed dead code; Sorts.of_sort_derivation: removed unused pp;
2009-09-29 wenzelm 2009-09-29 modernized Balanced_Tree;
2009-07-26 wenzelm 2009-07-26 Goal.finish: explicit context for printing;
2009-07-07 wenzelm 2009-07-07 add_classrel/arity: strip_shyps of stored result;
2009-07-06 wenzelm 2009-07-06 clarified Thm.of_class/of_sort/class_triv;
2009-07-06 wenzelm 2009-07-06 renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 wenzelm 2009-07-02 renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
2009-05-24 haftmann 2009-05-24 tuned class user space type system code
2009-05-20 haftmann 2009-05-20 avoid potential problem with stale theory
2009-04-17 haftmann 2009-04-17 formal declaration of undefined parameters after class instantiation
2009-03-13 haftmann 2009-03-13 coherent binding policy with primitive target operations
2009-03-12 wenzelm 2009-03-12 renamed sticky_prefix to mandatory_path;
2009-03-12 wenzelm 2009-03-12 replaced old-style add_path/no_base_names by sticky_prefix;
2009-03-08 wenzelm 2009-03-08 moved basic algebra of long names from structure NameSpace to Long_Name;
2009-03-07 wenzelm 2009-03-07 more uniform handling of binding in targets and derived elements;
2009-03-05 wenzelm 2009-03-05 renamed NameSpace.base to NameSpace.base_name; renamed NameSpace.map_base to NameSpace.map_base_name; eliminated alias Sign.base_name = NameSpace.base_name;
2009-03-04 haftmann 2009-03-04 merged
2009-03-04 haftmann 2009-03-04 explicit error message for `improper` instances lacking explicit instance parameter constants
2009-03-03 wenzelm 2009-03-03 Thm.binding;
2009-01-21 haftmann 2009-01-21 binding replaces bstring
2009-01-17 haftmann 2009-01-17 close derivation of classrels
2008-12-04 haftmann 2008-12-04 cleaned up binding module and related code
2008-09-03 wenzelm 2008-09-03 Sign.declare_const: Name.binding;
2008-09-02 wenzelm 2008-09-02 explicit type Name.binding for higher-specification elements;
2008-08-27 haftmann 2008-08-27 completing arities after subclass instance
2008-08-14 wenzelm 2008-08-14 moved basic thm operations from structure PureThy to Thm (cf. more_thm.ML);
2008-07-29 haftmann 2008-07-29 PureThy: dropped note_thmss_qualified, dropped _i suffix
2008-07-25 haftmann 2008-07-25 dropped PureThy.note; added PureThy.add_thm
2008-07-11 wenzelm 2008-07-11 Sorts.weaken: abstract argument;
2008-07-11 haftmann 2008-07-11 explicit completions of arities
2008-07-08 haftmann 2008-07-08 refined arity property concept
2008-06-30 haftmann 2008-06-30 tagged arities
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