| changeset 2033 | 74bd7bfb484b |
| parent 2012 | a48a6f88f76e |
| child 2372 | 06574b438b8f |
| 2032:5641981ec67d | 2033:74bd7bfb484b |
|---|---|
537 assumes fin: "finite S" |
537 assumes fin: "finite S" |
538 shows "supp (insert x S) = supp x \<union> supp S" |
538 shows "supp (insert x S) = supp x \<union> supp S" |
539 using fin |
539 using fin |
540 by (simp add: supp_of_fin_sets) |
540 by (simp add: supp_of_fin_sets) |
541 |
541 |
542 |
|
542 end |
543 end |