--- a/NEWS Sat Mar 29 19:14:16 2008 +0100
+++ b/NEWS Sat Mar 29 19:24:57 2008 +0100
@@ -32,7 +32,7 @@
* Eliminated destructive theorem database. Potential INCOMPATIBILITY,
really need to observe linear functional update of theories.
-* Commands 'use' and 'ML' are now purely functional, opearing on
+* Commands 'use' and 'ML' are now purely functional, operating on
theory/local_theory. Removed former 'ML_setup' (on theory), use 'ML'
instead. Added 'ML_val' as mere diagnostic replacement for 'ML'.
INCOMPATIBILITY.