equal
deleted
inserted
replaced
86 const Set.remove |
86 const Set.remove |
87 thm remove_def ~> Set.remove_eq [simp] |
87 thm remove_def ~> Set.remove_eq [simp] |
88 |
88 |
89 const Set.filter |
89 const Set.filter |
90 thm filter_def → Set.filter_eq [simp] |
90 thm filter_def → Set.filter_eq [simp] |
|
91 |
|
92 const [List.]can_select ~> Set.can_select |
|
93 thm can_select_def ~> Set.can_select_iff [simp] |
91 |
94 |
92 The _def suffix for characteristic theorems is avoided to emphasize that these |
95 The _def suffix for characteristic theorems is avoided to emphasize that these |
93 auxiliary operations are candidates for unfolding since they are variants |
96 auxiliary operations are candidates for unfolding since they are variants |
94 of existing logical concepts. The [simp] declarations try to move the attention |
97 of existing logical concepts. The [simp] declarations try to move the attention |
95 of the casual user away from these auxiliary operations; if they expose problems |
98 of the casual user away from these auxiliary operations; if they expose problems |