* Document preparation: renamed standard symbols \<ll> to \<lless> and
authorwenzelm
Wed, 24 Jan 2001 21:01:47 +0100
changeset 10976 0e7cf6f9fa29
parent 10975 32ba04b00ec0
child 10977 4b47d8aaf5af
* Document preparation: renamed standard symbols \<ll> to \<lless> and \<gg> to \<ggreater>;
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 ***