NEWS
changeset 63059 3f577308551e
parent 63043 df83a961d3a8
child 63066 4b0ad6c5d1ca
--- a/NEWS	Tue Apr 26 21:46:12 2016 +0200
+++ b/NEWS	Tue Apr 26 22:39:17 2016 +0200
@@ -64,6 +64,9 @@
 'definition' and 'obtain'. It fits better into the Isar language than
 old 'def', which is now a legacy feature.
 
+* Command 'obtain' supports structured statements with 'if' / 'for'
+context.
+
 * Command '\<proof>' is an alias for 'sorry', with different
 typesetting. E.g. to produce proof holes in examples and documentation.