equal
deleted
inserted
replaced
23 |
23 |
24 lemma dlist_eqI: |
24 lemma dlist_eqI: |
25 "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys" |
25 "list_of_dlist dxs = list_of_dlist dys \<Longrightarrow> dxs = dys" |
26 by (simp add: dlist_eq_iff) |
26 by (simp add: dlist_eq_iff) |
27 |
27 |
28 text \<open>Formal, totalized constructor for @{typ "'a dlist"}:\<close> |
28 text \<open>Formal, totalized constructor for \<^typ>\<open>'a dlist\<close>:\<close> |
29 |
29 |
30 definition Dlist :: "'a list \<Rightarrow> 'a dlist" where |
30 definition Dlist :: "'a list \<Rightarrow> 'a dlist" where |
31 "Dlist xs = Abs_dlist (remdups xs)" |
31 "Dlist xs = Abs_dlist (remdups xs)" |
32 |
32 |
33 lemma distinct_list_of_dlist [simp, intro]: |
33 lemma distinct_list_of_dlist [simp, intro]: |