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.