# HG changeset patch
# User wenzelm
# Date 1128718757 -7200
# Node ID 274eaa114c6db6a934fce25f79a23a7d549c53bd
# Parent  407bea05c2da76500d3c16e94132d817cb3e5a30
tuned;

diff -r 407bea05c2da -r 274eaa114c6d Admin/website/installation_notes_cygwin.html
--- a/Admin/website/installation_notes_cygwin.html	Fri Oct 07 22:59:15 2005 +0200
+++ b/Admin/website/installation_notes_cygwin.html	Fri Oct 07 22:59:17 2005 +0200
@@ -199,7 +199,7 @@
       script, e.&nbsp;g.</p>
     
       <blockquote>
-        <tt>@bash startx -geometry 30x4 -iconic -e Isabell</tt>
+        <tt>@bash startx -geometry 30x4 -iconic -e Isabelle</tt>
       </blockquote>
       
       <p>and assigning a shortcut in the start menu to it.</p>
diff -r 407bea05c2da -r 274eaa114c6d NEWS
--- a/NEWS	Fri Oct 07 22:59:15 2005 +0200
+++ b/NEWS	Fri Oct 07 22:59:17 2005 +0200
@@ -14,10 +14,12 @@
 * Input syntax now supports dummy variable binding "%_. b", where the
 body does not mention the bound variable.  Note that dummy patterns
 implicitly depend on their context of bounds, which makes "{_. _}"
-match any set comprehension as expected.
-
-* Removed obsolete syntactic constant _K and its associated parse
-translation.  INCOMPATIBILITY, use dummy abstraction instead, for
+match any set comprehension as expected.  Potential INCOMPATIBILITY --
+parse translations need to cope with syntactic constant "_idtdummy" in
+the binding position.
+
+* Removed obsolete syntactic constant "_K" and its associated parse
+translation.  INCOMPATIBILITY -- use dummy abstraction instead, for
 example "A -> B" => "Pi A (%_. B)".