NEWS
changeset 55385 169e12bbf9a3
parent 55316 885500f4aa6a
child 55425 7a3e78ee813b
     1.1 --- a/NEWS	Mon Feb 10 22:07:50 2014 +0100
     1.2 +++ b/NEWS	Mon Feb 10 22:08:18 2014 +0100
     1.3 @@ -44,6 +44,16 @@
     1.4  
     1.5  *** Pure ***
     1.6  
     1.7 +* Low-level type-class commands 'classes', 'classrel', 'arities' have
     1.8 +been discontinued to avoid the danger of non-trivial axiomatization
     1.9 +that is not immediately visible.  INCOMPATIBILITY, use regular
    1.10 +'instance' with proof.  The required OFCLASS(...) theorem might be
    1.11 +postulated via 'axiomatization' beforehand, or the proof finished
    1.12 +trivially if the underlying class definition is made vacuous (without
    1.13 +any assumptions).  See also Isabelle/ML operations
    1.14 +Axclass.axiomatize_class, Axclass.axiomatize_classrel,
    1.15 +Axclass.axiomatize_arity.
    1.16 +
    1.17  * Attributes "where" and "of" allow an optional context of local
    1.18  variables ('for' declaration): these variables become schematic in the
    1.19  instantiated theorem.