--- a/NEWS Wed Aug 30 17:55:12 2000 +0200
+++ b/NEWS Wed Aug 30 18:05:20 2000 +0200
@@ -84,9 +84,9 @@
*** Document preparation ***
* formal comments (text blocks etc.) in new-style theories may now
-contain antiquotations of thm/prop/term/typ to be presented according
-to latex print mode; concrete syntax is like this: @{term[show_types]
-"f(x) = a + x"};
+contain antiquotations of thm/prop/term/typ/text to be presented
+according to latex print mode; concrete syntax is like this:
+@{term[show_types] "f(x) = a + x"};
* isatool mkdir provides easy setup of Isabelle session directories,
including proper document sources;