# HG changeset patch
# User wenzelm
# Date 1190838480 -7200
# Node ID ef479bae1999c243a8d3e408c3e5b3f6664a656d
# Parent  92767beff42df1bb3534a8cec9c617eaae8348af
tuned;

diff -r 92767beff42d -r ef479bae1999 NEWS
--- a/NEWS	Wed Sep 26 22:27:44 2007 +0200
+++ b/NEWS	Wed Sep 26 22:28:00 2007 +0200
@@ -408,7 +408,7 @@
 'translations' with explicit "CONST" markup to accommodate this.
 
 * Pure/Isar: unified syntax for new-style specification mechanisms (e.g.
-'definition', 'abbreviation', or 'inductive' in HOL) admits type
+'definition', 'abbreviation', or 'inductive' in HOL) admits full type
 inference and dummy patterns ("_"). For example:
 
   definition "K x _ = x"