| changeset 18367 | c209f4b61b51 |
| parent 18308 | f18a54840629 |
| child 18370 | db5900e7c6c9 |
--- 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).