--- 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).