src/Pure/axclass.ML
2010-04-25 ago classrel and arity completion by krauss/schropp;
2010-04-11 ago Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-25 ago Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS);
2010-03-25 ago removed unused AxClass.of_sort derivation;
2010-03-22 ago inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;
2010-03-22 ago replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-21 ago Logic.mk_of_sort convenience;
2010-03-20 ago renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-09 ago added ProofContext.tsig_of -- proforma version for local name space only, not logical content;
2010-02-19 ago Thm.def_binding;
2010-02-18 ago axclass: more precise treatment of naming vs. binding;
2010-02-07 ago renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-01-04 ago discontinued old TheoryDataFun, but retain Theory_Data_PP with is Pretty.pp argument to merge (still required in exotic situations -- hard to get rid of);
2010-01-04 ago dropped copy operation for legacy TheoryDataFun
2009-11-30 ago dropped some unused bindings
2009-10-29 ago eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
2009-10-28 ago conceal internal bindings;
2009-10-25 ago eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 ago maintain theory name via name space, not tags;
2009-10-22 ago explicit close_derivation
2009-10-17 ago indicate CRITICAL nature of various setmp combinators;
2009-09-30 ago removed dead code;
2009-09-29 ago modernized Balanced_Tree;
2009-07-26 ago Goal.finish: explicit context for printing;
2009-07-07 ago add_classrel/arity: strip_shyps of stored result;
2009-07-06 ago clarified Thm.of_class/of_sort/class_triv;
2009-07-06 ago renamed inclass/Inclass to of_class/OfClass, in accordance to of_sort;
2009-07-02 ago renamed Drule.sort_triv to Thm.sort_triv (cf. more_thm.ML);
2009-05-24 ago tuned class user space type system code
2009-05-20 ago avoid potential problem with stale theory
2009-04-17 ago formal declaration of undefined parameters after class instantiation
2009-03-13 ago coherent binding policy with primitive target operations
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