equal
deleted
inserted
replaced
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. |
143 |
146 |
144 * Alternative iff syntax "A <-> B" for equality on bool (with priority |
147 * Alternative iff syntax "A <-> B" for equality on bool (with priority |
145 25 like -->); output depends on the "iff" print_mode, the default is |
148 25 like -->); output depends on the "iff" print_mode, the default is |
146 "A = B" (with priority 50). |
149 "A = B" (with priority 50). |
147 |
150 |