equal
deleted
inserted
replaced
184 Requires a proof bundle, which is available as an external component. |
184 Requires a proof bundle, which is available as an external component. |
185 Discontinued old (and mostly dead) Importer for HOL4 and HOL Light. |
185 Discontinued old (and mostly dead) Importer for HOL4 and HOL Light. |
186 INCOMPATIBILITY. |
186 INCOMPATIBILITY. |
187 |
187 |
188 * New type synonym 'a rel = ('a * 'a) set |
188 * New type synonym 'a rel = ('a * 'a) set |
|
189 |
|
190 * Typedef with implicit set definition is considered legacy. Use |
|
191 "typedef (open)" form instead, which will eventually become the |
|
192 default. |
189 |
193 |
190 * More default pred/set conversions on a couple of relation operations |
194 * More default pred/set conversions on a couple of relation operations |
191 and predicates. Added powers of predicate relations. Consolidation |
195 and predicates. Added powers of predicate relations. Consolidation |
192 of some relation theorems: |
196 of some relation theorems: |
193 |
197 |