NEWS
changeset 18370 db5900e7c6c9
parent 18367 c209f4b61b51
child 18399 651438736fa1
equal deleted inserted replaced
18369:694ea14ab4f2 18370:db5900e7c6c9
   138 translation.  INCOMPATIBILITY -- use dummy abstraction instead, for
   138 translation.  INCOMPATIBILITY -- use dummy abstraction instead, for
   139 example "A -> B" => "Pi A (%_. B)".
   139 example "A -> B" => "Pi A (%_. B)".
   140 
   140 
   141 
   141 
   142 *** HOL ***
   142 *** HOL ***
   143 
       
   144 * Theorem 'swap' is no longer bound at the ML top-level.  INCOMPATIBILITY, use
       
   145 Classical.swap instead.
       
   146 
   143 
   147 * Alternative iff syntax "A <-> B" for equality on bool (with priority
   144 * Alternative iff syntax "A <-> B" for equality on bool (with priority
   148 25 like -->); output depends on the "iff" print_mode, the default is
   145 25 like -->); output depends on the "iff" print_mode, the default is
   149 "A = B" (with priority 50).
   146 "A = B" (with priority 50).
   150 
   147