| changeset 2463 | 217149972715 |
| parent 2462 | 937b6088a3a0 |
| child 2466 | 47c840599a6b |
| 2462:937b6088a3a0 | 2463:217149972715 |
|---|---|
546 lemma supp_set: |
546 lemma supp_set: |
547 fixes xs :: "('a::fs) list" |
547 fixes xs :: "('a::fs) list" |
548 shows "supp (set xs) = supp xs" |
548 shows "supp (set xs) = supp xs" |
549 apply(induct xs) |
549 apply(induct xs) |
550 apply(simp add: supp_set_empty supp_Nil) |
550 apply(simp add: supp_set_empty supp_Nil) |
551 apply(simp add: supp_Cons finite_set supp_of_fin_insert) |
551 apply(simp add: supp_Cons supp_of_fin_insert) |
552 done |
552 done |
553 |
553 |
554 end |
554 end |