# HG changeset patch
# User wenzelm
# Date 953403416 -3600
# Node ID daaedc7b56a9dc4cd2a9e7d460e8697748af9e06
# Parent  062e6cd7853415429e013fb405dbce8a155a2a59
tuned;

diff -r 062e6cd78534 -r daaedc7b56a9 NEWS
--- a/NEWS	Sat Mar 18 19:11:34 2000 +0100
+++ b/NEWS	Sat Mar 18 19:16:56 2000 +0100
@@ -9,30 +9,30 @@
 
 * HOL: the constant for f``x is now "image" rather than "op ``".
 
-* HOL: exhaust_tac on datatypes superceded by new case_tac;
+* HOL: exhaust_tac on datatypes superceded by new generic case_tac;
 
-* ML: PureThy.add_thms/add_axioms/add_defs now return theorems;
+* ML: PureThy.add_thms/add_axioms/add_defs return theorems as well;
 
 
 *** Document preparation ***
 
 * isatool mkdir provides easy setup of Isabelle session directories,
-including proper documents;
+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
 of isatool usedir;
 
-* old-style theories now produce (crude) LaTeX sources as well;
+* old-style theories now produce (crude) LaTeX output as well;
 
 
 *** Isar ***
 
 * Pure now provides its own version of intro/elim/dest attributes;
 useful for building new logics, but beware of confusion with the
-Provers/classical ones!
+Provers/classical ones;
 
-* Pure: new 'obtain' language element supports generalized existence
+* Pure: new 'obtain' language element supports generalized elimination
 proofs;
 
 * Pure: scalable support for case-analysis type proofs: new 'case'
@@ -53,19 +53,19 @@
 
 * names of theorems etc. may be natural numbers as well;
 
-* intro/elim/dest attributes: changed ! / !! flags to ? / ??;
+* Provers: intro/elim/dest attributes: changed ! / !! flags to ? / ??;
 
 * 'pr' command: optional goals_limit argument;
 
 * diagnostic commands 'pr', 'thm', 'prop', 'term', 'typ' admit
-additional print modes to be specified; e.g. pr(latex) will print
-proof according to the Isabelle LaTeX style;
+additional print modes to be specified; e.g. "pr(latex)" will print
+proof state according to the Isabelle LaTeX style;
 
 
 *** HOL ***
 
-* Algebra: new theory of rings and univariate polynomials, by Clemens
-Ballarin;
+* HOL/Algebra: new theory of rings and univariate polynomials, by
+Clemens Ballarin;
 
 * HOL/record: fixed select-update simplification procedure to handle
 extended records as well; admit "r" as field name;
@@ -75,18 +75,16 @@
 
 * new version of "case_tac" subsumes both boolean case split and
 "exhaust_tac" on datatypes; INCOMPATIBILITY: exhaust_tac no longer
-exists, may define val exhaust_tac = case_tac for quick-and-dirty
-portability;
+exists, may define val exhaust_tac = case_tac for ad-hoc portability;
 
 
 *** General ***
 
 * compression of ML heaps images may now be controlled via -c option
-of isabelle and isatool usedir;
+of isabelle and isatool usedir (currently only observed by Poly/ML);
 
-* new ML combinators |>> and |>>> for incremental transformations with
-secondary results (e.g. certain theory extensions):
-
+* ML: new combinators |>> and |>>> for incremental transformations
+with secondary results (e.g. certain theory extensions):