# HG changeset patch
# User wenzelm
# Date 1134042602 -3600
# Node ID c209f4b61b5101328056c0ce7c3c7733bf70786a
# Parent  78b4f225b64041535f1a4f501eeb07664d65ada3
* HOL: Theorem 'swap' is no longer bound at the ML top-level.

diff -r 78b4f225b640 -r c209f4b61b51 NEWS
--- a/NEWS	Thu Dec 08 10:17:21 2005 +0100
+++ b/NEWS	Thu Dec 08 12:50:02 2005 +0100
@@ -141,6 +141,9 @@
 
 *** 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).