src/HOL/Library/Dlist.thy
changeset 37595 9591362629e3
parent 37473 013f78aed840
child 37765 26bdfb7b680b
     1.1 --- a/src/HOL/Library/Dlist.thy	Fri Jun 25 07:19:21 2010 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Mon Jun 28 15:32:06 2010 +0200
     1.3 @@ -122,7 +122,7 @@
     1.4    next
     1.5      case (insert x xs)
     1.6      then have "\<not> member (Dlist xs) x" and "P (Dlist xs)"
     1.7 -      by (simp_all add: member_def mem_iff)
     1.8 +      by (simp_all add: member_def List.member_def)
     1.9      with insrt have "P (insert x (Dlist xs))" .
    1.10      with insert show ?case by (simp add: insert_def distinct_remdups_id)
    1.11    qed
    1.12 @@ -144,7 +144,7 @@
    1.13      case (Cons x xs)
    1.14      with dxs distinct have "\<not> member (Dlist xs) x"
    1.15        and "dxs = insert x (Dlist xs)"
    1.16 -      by (simp_all add: member_def mem_iff insert_def distinct_remdups_id)
    1.17 +      by (simp_all add: member_def List.member_def insert_def distinct_remdups_id)
    1.18      with insert show P .
    1.19    qed
    1.20  qed
    1.21 @@ -205,7 +205,7 @@
    1.22  
    1.23  lemma is_empty_Set [code]:
    1.24    "Fset.is_empty (Set dxs) \<longleftrightarrow> null dxs"
    1.25 -  by (simp add: null_def null_empty member_set)
    1.26 +  by (simp add: null_def List.null_def member_set)
    1.27  
    1.28  lemma bot_code [code]:
    1.29    "bot = Set empty"