2010-05-15 wenzelm 2010-05-15 eliminated redundant runtime checks;
2010-05-15 krauss 2010-05-15 normalize atyp names after unconstrainT, which may rename atyps arbitrarily;
2010-05-13 wenzelm 2010-05-13 the_classrel/the_arity: avoid Thm.transfer for proofterm version -- theory might already have become stale within the proof_body future;
2010-05-09 wenzelm 2010-05-09 just one version of Thm.unconstrainT, which affects all variables; temporary workaround for Nbe.lift_triv_classes_conv;
2010-05-08 wenzelm 2010-05-08 back-patching of axclass proofs;
2010-05-03 wenzelm 2010-05-03 renamed ProofContext.init to ProofContext.init_global to emphasize that this is not the real thing;
2010-04-28 wenzelm 2010-04-28 made SML/NJ happy;
2010-04-27 wenzelm 2010-04-27 removed obsolete sanity check -- Sign.certify_sort is stable;
2010-04-27 wenzelm 2010-04-27 tuned signature;
2010-04-27 wenzelm 2010-04-27 tuned classrel completion -- bypass composition with reflexive edges;
2010-04-27 wenzelm 2010-04-27 tuned diff_classrels -- avoid slightly inefficient Symreltab.keys;
2010-04-27 wenzelm 2010-04-27 tuned aritiy completion -- slightly less intermediate data structures;
2010-04-27 wenzelm 2010-04-27 clarified proven results: store thm only and retrieve proof later via Thm.proof_of (this may also impact parallelism, because internal join_proofs is deferred);
2010-04-27 wenzelm 2010-04-27 misc tuning and simplification;
2010-04-26 wenzelm 2010-04-26 removed unused AxClass.class_intros;
2010-04-25 wenzelm 2010-04-25 renamed Drule.unconstrainTs to Thm.unconstrain_allTs to accomdate the version by krauss/schropp; less pervasive names;
2010-04-25 wenzelm 2010-04-25 more systematic treatment of data -- avoid slightly odd nested tuples here; tuned;
2010-04-25 wenzelm 2010-04-25 replaced Sorts.rep_algebra by slightly more abstract selectors classes_of/arities_of;
2010-04-25 wenzelm 2010-04-25 misc tuning and simplification;
2010-04-25 wenzelm 2010-04-25 simplified some private bindings;
2010-04-25 wenzelm 2010-04-25 classrel and arity completion by krauss/schropp;
2010-04-11 wenzelm 2010-04-11 Thm.add_axiom/add_def: return internal name of foundational axiom;
2010-03-25 wenzelm 2010-03-25 Sorts.of_sort_derivation: do not use slow Graph.irreducible_paths here, which not always needed (SUBTLE CHANGE IN SEMANTICS); officially export weaken as Sorts.classrel_derivation; tuned comments;
2010-03-25 wenzelm 2010-03-25 removed unused AxClass.of_sort derivation;
2010-03-22 wenzelm 2010-03-22 inlined version of old-style Drule.add_axioms -- Specification.axiom is not bootstrapped yet;
2010-03-22 wenzelm 2010-03-22 replaced PureThy.add_axioms by more basic Drule.add_axiom, which is old-style nonetheless;
2010-03-21 wenzelm 2010-03-21 Logic.mk_of_sort convenience;
2010-03-20 wenzelm 2010-03-20 renamed varify/unvarify operations to varify_global/unvarify_global to emphasize that these only work in a global situation;
2010-03-09 wenzelm 2010-03-09 added ProofContext.tsig_of -- proforma version for local name space only, not logical content; added ProofContext.read_type_name_proper; localized ProofContext.read_class/read_arity/cert_arity; localized ProofContext.class_space/type_space etc.;
2010-02-19 wenzelm 2010-02-19 Thm.def_binding;
2010-02-18 wenzelm 2010-02-18 axclass: more precise treatment of naming vs. binding;
2010-02-07 wenzelm 2010-02-07 renamed old-style Drule.standard to Drule.export_without_context, to emphasize that this is in no way a standard operation;
2010-01-04 wenzelm 2010-01-04 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 haftmann 2010-01-04 dropped copy operation for legacy TheoryDataFun
2009-11-30 haftmann 2009-11-30 dropped some unused bindings
2009-10-29 wenzelm 2009-10-29 eliminated obsolete/unused Thm.kind_internal/is_internal etc.;
2009-10-28 wenzelm 2009-10-28 conceal internal bindings;
2009-10-25 wenzelm 2009-10-25 eliminated obsolete tags for types/consts -- now handled via name space, in strongly typed fashion;
2009-10-25 wenzelm 2009-10-25 maintain theory name via name space, not tags; AxClass.thynames_of_arity: explicit theory name, not tags;
2009-10-22 haftmann 2009-10-22 explicit close_derivation
2009-10-17 wenzelm 2009-10-17 indicate CRITICAL nature of various setmp combinators;
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;