1.1 --- a/src/HOL/Library/Dlist_Cset.thy	Tue Jun 07 11:11:01 2011 +0200
     1.2 +++ b/src/HOL/Library/Dlist_Cset.thy	Tue Jun 07 11:12:05 2011 +0200
     1.3 @@ -3,21 +3,21 @@
     1.4  header {* Canonical implementation of sets by distinct lists *}
     1.5  
     1.6  theory Dlist_Cset
     1.7 -imports Dlist Cset
     1.8 +imports Dlist List_Cset
     1.9  begin
    1.10  
    1.11  definition Set :: "'a dlist \<Rightarrow> 'a Cset.set" where
    1.12 -  "Set dxs = Cset.set (list_of_dlist dxs)"
    1.13 +  "Set dxs = List_Cset.set (list_of_dlist dxs)"
    1.14  
    1.15  definition Coset :: "'a dlist \<Rightarrow> 'a Cset.set" where
    1.16 -  "Coset dxs = Cset.coset (list_of_dlist dxs)"
    1.17 +  "Coset dxs = List_Cset.coset (list_of_dlist dxs)"
    1.18  
    1.19  code_datatype Set Coset
    1.20  
    1.21  declare member_code [code del]
    1.22 -declare Cset.is_empty_set [code del]
    1.23 -declare Cset.empty_set [code del]
    1.24 -declare Cset.UNIV_set [code del]
    1.25 +declare List_Cset.is_empty_set [code del]
    1.26 +declare List_Cset.empty_set [code del]
    1.27 +declare List_Cset.UNIV_set [code del]
    1.28  declare insert_set [code del]
    1.29  declare remove_set [code del]
    1.30  declare compl_set [code del]
    1.31 @@ -50,11 +50,11 @@
    1.32    by (simp add: Coset_def member_set not_set_compl)
    1.33  
    1.34  lemma Set_dlist_of_list [code]:
    1.35 -  "Cset.set xs = Set (dlist_of_list xs)"
    1.36 +  "List_Cset.set xs = Set (dlist_of_list xs)"
    1.37    by (rule Cset.set_eqI) simp
    1.38  
    1.39  lemma Coset_dlist_of_list [code]:
    1.40 -  "Cset.coset xs = Coset (dlist_of_list xs)"
    1.41 +  "List_Cset.coset xs = Coset (dlist_of_list xs)"
    1.42    by (rule Cset.set_eqI) simp
    1.43  
    1.44  lemma is_empty_Set [code]: