--- a/NEWS Sat Oct 17 22:58:18 2009 +0200
+++ b/NEWS Sat Oct 17 23:07:53 2009 +0200
@@ -27,6 +27,14 @@
interpretation.
+*** document preparation ***
+
+* New generalized style concept for printing terms:
+write @{foo (style) ...} instead of @{foo_style style ...}
+(old form is still retained for backward compatibility).
+Styles can be also applied for antiquotations prop, term_type and typeof.
+
+
*** HOL ***
* Most rules produced by inductive and datatype package
@@ -245,6 +253,9 @@
Syntax.pretty_typ/term directly, preferably with proper context
instead of global theory.
+* Operations of structure Skip_Proof (formerly SkipProof) no longer
+require quick_and_dirty mode, which avoids critical setmp.
+
*** System ***