equal
deleted
inserted
replaced
133 Isabelle2011-1 before jumping right into the current release. |
133 Isabelle2011-1 before jumping right into the current release. |
134 |
134 |
135 * Code generation by default implements sets as container type rather |
135 * Code generation by default implements sets as container type rather |
136 than predicates. INCOMPATIBILITY. |
136 than predicates. INCOMPATIBILITY. |
137 |
137 |
138 * New proof import from HOL Light, cf. HOL/Import. Requires a proof |
138 * New proof import from HOL Light: Faster, simpler, and more scalable. |
139 bundle, which is available as an external component. Removed old (and |
139 Requires a proof bundle, which is available as an external component. |
140 mostly dead) Importer for HOL4 and HOL Light. INCOMPATIBILITY. |
140 Removed old (and mostly dead) Importer for HOL4 and HOL Light. |
|
141 INCOMPATIBILITY. |
141 |
142 |
142 * New type synonym 'a rel = ('a * 'a) set |
143 * New type synonym 'a rel = ('a * 'a) set |
143 |
144 |
144 * Theory Divides: Discontinued redundant theorems about div and mod. |
145 * Theory Divides: Discontinued redundant theorems about div and mod. |
145 INCOMPATIBILITY, use the corresponding generic theorems instead. |
146 INCOMPATIBILITY, use the corresponding generic theorems instead. |