--- a/NEWS Thu Jun 29 22:32:45 2000 +0200
+++ b/NEWS Thu Jun 29 22:35:45 2000 +0200
@@ -57,6 +57,11 @@
*** 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"};
+
* isatool mkdir provides easy setup of Isabelle session directories,
including proper document sources;
@@ -105,6 +110,12 @@
* Pure: removed obsolete 'transfer' attribute (transfer of thms to the
current context is now done automatically);
+* Pure: theory command 'hide' removes declarations from
+class/type/const name spaces;
+
+* Pure: theory command 'method_setup' provides a simple interface for
+definining proof methods in ML;
+
* Provers: splitter support (via 'split' attribute and 'simp' method
modifier); 'simp' method: 'only:' modifier removes loopers as well
(including splits);
@@ -135,10 +146,7 @@
all goals, or explicit goal specifier (tactic emulation); thus 'proof
method scripts' have to be in depth-first order;
-* tuned 'let' syntax: replace 'as' keyword by 'and';
-
-* theory command 'hide' removes declarations from class/type/const
-name spaces;
+* tuned 'let' syntax: replaced 'as' keyword by 'and';
*** HOL ***