81 Non-trivial INCOMPATIBILITY. For developments keeping predicates and |
81 Non-trivial INCOMPATIBILITY. For developments keeping predicates and |
82 sets separate, it is often sufficient to rephrase sets S accidentally |
82 sets separate, it is often sufficient to rephrase sets S accidentally |
83 used as predicates by "%x. x : S" and predicates P accidentally used |
83 used as predicates by "%x. x : S" and predicates P accidentally used |
84 as sets by "{x. P x}". Corresponding proofs in a first step should be |
84 as sets by "{x. P x}". Corresponding proofs in a first step should be |
85 pruned from any tinkering with former theorems mem_def and |
85 pruned from any tinkering with former theorems mem_def and |
86 Collect_def. For developments which deliberately mixed predicates and |
86 Collect_def as far as possible. |
|
87 For developments which deliberately mixed predicates and |
87 sets, a planning step is necessary to determine what should become a |
88 sets, a planning step is necessary to determine what should become a |
88 predicate and what a set. It can be helpful to carry out that step in |
89 predicate and what a set. It can be helpful to carry out that step in |
89 Isabelle2011-1 before jumping right into the current release. |
90 Isabelle2011-1 before jumping right into the current release. |
|
91 |
|
92 * Code generation by default implements sets as container type rather |
|
93 than predicates. INCOMPATIBILITY. |
90 |
94 |
91 * New type synonym 'a rel = ('a * 'a) set |
95 * New type synonym 'a rel = ('a * 'a) set |
92 |
96 |
93 * More default pred/set conversions on a couple of relation operations |
97 * More default pred/set conversions on a couple of relation operations |
94 and predicates. Consolidation of some relation theorems: |
98 and predicates. Consolidation of some relation theorems: |