removed hint for Classical.swap, which is not really user-level anyway;
authorwenzelm
Thu, 08 Dec 2005 20:15:34 +0100
changeset 18370 db5900e7c6c9
parent 18369 694ea14ab4f2
child 18371 d93fdf00f8a6
removed hint for Classical.swap, which is not really user-level anyway;
NEWS
--- a/NEWS	Thu Dec 08 12:50:04 2005 +0100
+++ b/NEWS	Thu Dec 08 20:15:34 2005 +0100
@@ -141,9 +141,6 @@
 
 *** HOL ***
 
-* Theorem 'swap' is no longer bound at the ML top-level.  INCOMPATIBILITY, use
-Classical.swap instead.
-
 * Alternative iff syntax "A <-> B" for equality on bool (with priority
 25 like -->); output depends on the "iff" print_mode, the default is
 "A = B" (with priority 50).