author | wenzelm |
Thu, 08 Dec 2005 12:50:02 +0100 | |
changeset 18367 | c209f4b61b51 |
parent 18366 | 78b4f225b640 |
child 18368 | 2f9b2539c5bb |
--- 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).