equal
deleted
inserted
replaced
1142 |
1142 |
1143 lemma Sigma_Union: |
1143 lemma Sigma_Union: |
1144 "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)" |
1144 "Sigma (\<Union>X) B = (\<Union>A\<in>X. Sigma A B)" |
1145 by blast |
1145 by blast |
1146 |
1146 |
|
1147 lemma Pair_vimage_Sigma: "Pair x -` Sigma A f = (if x \<in> A then f x else {})" |
|
1148 by auto |
|
1149 |
1147 text \<open> |
1150 text \<open> |
1148 Non-dependent versions are needed to avoid the need for higher-order |
1151 Non-dependent versions are needed to avoid the need for higher-order |
1149 matching, especially when the rules are re-oriented. |
1152 matching, especially when the rules are re-oriented. |
1150 \<close> |
1153 \<close> |
1151 |
1154 |