NEWS
changeset 60094 96a4765ba7d1
parent 60093 c48d536231fe
child 60106 e0d1d9203275
     1.1 --- a/NEWS	Thu Apr 16 13:48:10 2015 +0200
     1.2 +++ b/NEWS	Thu Apr 16 14:18:32 2015 +0200
     1.3 @@ -398,6 +398,9 @@
     1.4  derivatives) instead, which is not affected by the change. Potential
     1.5  INCOMPATIBILITY in rare applications of Name_Space.intern.
     1.6  
     1.7 +* Subtle change of error semantics of Toplevel.proof_of: regular user
     1.8 +ERROR instead of internal Toplevel.UNDEF.
     1.9 +
    1.10  * Basic combinators map, fold, fold_map, split_list, apply are available
    1.11  as parameterized antiquotations, e.g. @{map 4} for lists of quadruples.
    1.12