diff -r aaa9933039b3 -r 5ab0f8859f9f NEWS
--- a/NEWS	Mon Apr 26 21:36:44 2010 +0200
+++ b/NEWS	Mon Apr 26 21:45:08 2010 +0200
@@ -103,6 +103,9 @@
 datatype constructors have been renamed from InfixName to Infix etc.
 Minor INCOMPATIBILITY.
 
+* Command 'example_proof' opens an empty proof body.  This allows to
+experiment with Isar, without producing any persistent result.
+
 * Commands 'type_notation' and 'no_type_notation' declare type syntax
 within a local theory context, with explicit checking of the
 constructors involved (in contrast to the raw 'syntax' versions).