# 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