NEWS

 * LaTeX: several improvements of isabelle.sty;
 
 
 *** 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;
 
 * generated LaTeX sources are now deleted after successful run
 (isatool document -c); may retain a copy somewhere else via -D option

 name 'antecedent';
 
 * 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);
 
 * HOL: new proof method 'cases' and improved version of 'induct' now

 
 * simplified (more robust) goal selection of proof methods: 1st goal,
 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 ***
 
 * HOL/Prolog: a (bare-bones) implementation of Lambda-Prolog