# HG changeset patch # User wenzelm # Date 1190838464 -7200 # Node ID 92767beff42df1bb3534a8cec9c617eaae8348af # Parent 3a55ee2cae70444e22c0df642db7fa896b7ad6fb tuned; diff -r 3a55ee2cae70 -r 92767beff42d NEWS --- a/NEWS Wed Sep 26 22:21:05 2007 +0200 +++ b/NEWS Wed Sep 26 22:27:44 2007 +0200 @@ -407,8 +407,8 @@ slightly different -- use 'notation' instead of raw 'syntax', and 'translations' with explicit "CONST" markup to accommodate this. -* Pure/Isar: unified syntax for new-style specification mechanisms -('definition', 'abbreviation', or 'inductive' in HOL) admits type +* Pure/Isar: unified syntax for new-style specification mechanisms (e.g. +'definition', 'abbreviation', or 'inductive' in HOL) admits type inference and dummy patterns ("_"). For example: definition "K x _ = x"