# HG changeset patch
# User wenzelm
# Date 1461836066 -7200
# Node ID 4b0ad6c5d1cad5cbb751e6e1c592e5597e6b1626
# Parent  3cb7b06d0a9f0938253fc119ebc9ac83c6033042
NEWS;

diff -r 3cb7b06d0a9f -r 4b0ad6c5d1ca NEWS
--- a/NEWS	Thu Apr 28 11:31:36 2016 +0200
+++ b/NEWS	Thu Apr 28 11:34:26 2016 +0200
@@ -59,6 +59,10 @@
 
 *** Isar ***
 
+* Many specification elements support structured statements with 'if'
+eigen-context, e.g. 'axiomatization', 'definition', 'inductive',
+'function'.
+
 * Command 'define' introduces a local (non-polymorphic) definition, with
 optional abstraction over local parameters. The syntax resembles
 'definition' and 'obtain'. It fits better into the Isar language than