| changeset 45990 | b7b905b23b2a |
| parent 45129 | 1fce03e3e8ad |
| child 47092 | fa3538d6004b |
| 45989:b39256df5f8a | 45990:b7b905b23b2a |
|---|---|
6 *) |
6 *) |
7 |
7 |
8 header {* Lists with distinct elements *} |
8 header {* Lists with distinct elements *} |
9 |
9 |
10 theory DList |
10 theory DList |
11 imports "~~/src/HOL/Library/Quotient_List" "~~/src/HOL/Library/More_List" |
11 imports "~~/src/HOL/Library/Quotient_List" |
12 begin |
12 begin |
13 |
13 |
14 text {* Some facts about lists *} |
14 text {* Some facts about lists *} |
15 |
15 |
16 lemma remdups_removeAll_commute[simp]: |
16 lemma remdups_removeAll_commute[simp]: |