| changeset 2050 | 8bd75f2fd7b0 |
| parent 2033 | 74bd7bfb484b |
| child 2372 | 06574b438b8f |
| 2049:38bbccdf9ff9 | 2050:8bd75f2fd7b0 |
|---|---|
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 |