# HG changeset patch
# User wenzelm
# Date 962310945 -7200
# Node ID 0ab3c81e94253f2e848af6d349def79a89f5f490
# Parent  16d88c5547bd30c197814d7531577cd0288b3d48
* 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"};
* Isar: theory command 'method_setup' provides a simple interface for
definining proof methods in ML;

diff -r 16d88c5547bd -r 0ab3c81e9425 NEWS
--- 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 ***