equal
deleted
inserted
replaced
133 |
133 |
134 * Code generation by default implements sets as container type rather |
134 * Code generation by default implements sets as container type rather |
135 than predicates. INCOMPATIBILITY. |
135 than predicates. INCOMPATIBILITY. |
136 |
136 |
137 * New type synonym 'a rel = ('a * 'a) set |
137 * New type synonym 'a rel = ('a * 'a) set |
|
138 |
|
139 * Theory Divides: Discontinued redundant theorems about div and mod. |
|
140 INCOMPATIBILITY, use the corresponding generic theorems instead. |
|
141 |
|
142 DIVISION_BY_ZERO ~> div_by_0, mod_by_0 |
|
143 zdiv_self ~> div_self |
|
144 zmod_self ~> mod_self |
|
145 zdiv_zero ~> div_0 |
|
146 zmod_zero ~> mod_0 |
|
147 zmod_zdiv_trivial ~> mod_div_trivial |
138 |
148 |
139 * More default pred/set conversions on a couple of relation operations |
149 * More default pred/set conversions on a couple of relation operations |
140 and predicates. Consolidation of some relation theorems: |
150 and predicates. Consolidation of some relation theorems: |
141 |
151 |
142 converse_def ~> converse_unfold |
152 converse_def ~> converse_unfold |