# HG changeset patch
# User wenzelm
# Date 980366507 -3600
# Node ID 0e7cf6f9fa29e610eb5ef207a9f2470ac40245a5
# Parent  32ba04b00ec0e0c766dca38dba3c54adaf7f9791
* Document preparation: renamed standard symbols \<ll> to \<lless> and
\<gg> to \<ggreater>;

diff -r 32ba04b00ec0 -r 0e7cf6f9fa29 NEWS
--- a/NEWS	Wed Jan 24 20:57:19 2001 +0100
+++ b/NEWS	Wed Jan 24 21:01:47 2001 +0100
@@ -23,6 +23,9 @@
 consequence, it is no longer monotonic wrt. the local goal context
 (which is now passed through the inductive cases);
 
+* Document preparation: renamed standard symbols \<ll> to \<lless> and
+\<gg> to \<ggreater>;
+
 
 *** Document preparation ***