| changeset 35413 | 4c7cba1f7ce9 |
| parent 35401 | bfcbab8592ba |
| child 35436 | 38b291bb4a98 |
--- a/NEWS Mon Mar 01 17:07:36 2010 +0100 +++ b/NEWS Mon Mar 01 17:09:42 2010 +0100 @@ -51,6 +51,10 @@ datatype constructors have been renamed from InfixName to Infix etc. Minor INCOMPATIBILITY. +* Commands 'type_notation' and 'no_type_notation' declare type syntax +within a local theory context, with explicit checking of the +constructors involved (in contrast to the raw 'syntax' versions). + *** HOL ***