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