| changeset 385 | 7f8516ff408d |
| parent 363 | 0d6deecdb2eb |
| child 397 | cf3ca219c727 |
| 384:4629448c1bd9 | 385:7f8516ff408d |
|---|---|
1 theory Matcher2 |
1 ytheory Matcher2 |
2 imports "Main" |
2 imports "Main" |
3 begin |
3 begin |
4 |
4 |
5 lemma Suc_Union: |
5 lemma Suc_Union: |
6 "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))" |
6 "(\<Union> x\<le>Suc m. B x) = (B (Suc m) \<union> (\<Union> x\<le>m. B x))" |