equal
deleted
inserted
replaced
21 |
21 |
22 |
22 |
23 text {* Formal, totalized constructor for @{typ "'a dlist"}: *} |
23 text {* Formal, totalized constructor for @{typ "'a dlist"}: *} |
24 |
24 |
25 definition Dlist :: "'a list \<Rightarrow> 'a dlist" where |
25 definition Dlist :: "'a list \<Rightarrow> 'a dlist" where |
26 [code del]: "Dlist xs = Abs_dlist (remdups xs)" |
26 "Dlist xs = Abs_dlist (remdups xs)" |
27 |
27 |
28 lemma distinct_list_of_dlist [simp]: |
28 lemma distinct_list_of_dlist [simp]: |
29 "distinct (list_of_dlist dxs)" |
29 "distinct (list_of_dlist dxs)" |
30 using list_of_dlist [of dxs] by simp |
30 using list_of_dlist [of dxs] by simp |
31 |
31 |