# HG changeset patch # User wenzelm # Date 1146430199 -7200 # Node ID d5236f5b0a7110be291dfd6e755d95b0ec23a479 # Parent b386fcdc9945e38406af24bb3bfb011552573094 * Pure: axclasses now purely definitional; * Pure/kernel: consts certification ignores sort constraints; diff -r b386fcdc9945 -r d5236f5b0a71 NEWS --- a/NEWS Sat Apr 29 23:16:49 2006 +0200 +++ b/NEWS Sun Apr 30 22:49:59 2006 +0200 @@ -467,6 +467,17 @@ GenericDataFun. INCOMPATIBILITY, need to adapt attribute type declarations and definitions. +* Pure/kernel: consts certification ignores sort constraints given in +signature declarations. (This information is not relevant to the +logic, but only for type inference.) IMPORTANT INTERNAL CHANGE. + +* Pure: axiomatic type classes are now purely definitional, with +explicit proofs of class axioms and super class relations performed +internally. See Pure/axclass.ML for the main internal interfaces -- +notably AxClass.define_class supercedes AxClass.add_axclass, and +AxClass.axiomatize_class/classrel/arity supercede +Sign.add_classes/classrel/arities. + * Pure/Isar: Args/Attrib parsers operate on Context.generic -- global/local versions on theory vs. Proof.context have been discontinued; Attrib.syntax and Method.syntax have been adapted