* Calculation commands "moreover" and "also" no longer interfere with
current facts ("this"), admitting arbitrary combinations with "then"
and derived forms.

--- a/NEWS	Tue Apr 13 20:22:26 2004 +0200
+++ b/NEWS	Tue Apr 13 20:31:55 2004 +0200
@@ -10,7 +10,7 @@
   Replaces linorder.ML.
 
 * Pure: Greek letters (except small lambda, \<lambda>), as well as gothic
-  (\<aa>...\<zz>\<AA>...\<ZZ>), caligraphic (\<A>...\<Z>), and euler
+  (\<aa>...\<zz>\<AA>...\<ZZ>), calligraphic (\<A>...\<Z>), and euler
   (\<a>...\<z>), are now considered normal letters, and can therefore
   be used anywhere where an ASCII letter (a...zA...Z) has until
   now. COMPATIBILITY: This obviously changes the parsing of some
@@ -54,6 +54,7 @@
   (somewhat) independet of content. It is copied from lib/html/isabelle.css. 
   It can be changed to alter the colors/layout of generated pages.
 
+
 *** Isar ***
 
 * Tactic emulation methods rule_tac, erule_tac, drule_tac, frule_tac,
@@ -72,8 +73,9 @@
     theorems to have too special types in some circumstances.
   - "where" permits explicit instantiations of type variables.
 
-* Calculation commands "moreover" and "also":
-  Do not reset facts ("this") any more.
+* Calculation commands "moreover" and "also" no longer interfere with
+  current facts ("this"), admitting arbitrary combinations with "then"
+  and derived forms.
 
 * Locales:
   - Goal statements involving the context element "includes" no longer
@@ -100,6 +102,7 @@
 * HOL: Tactic emulation methods induct_tac and case_tac understand static
   (Isar) contexts.
 
+
 *** HOL ***
 
 * Simplifier: