src/HOL/Library/DAList.thy
changeset 46507 1b24c24017dd
parent 46238 9ace9e5b79be
child 47143 212f7a975d49
     1.1 --- a/src/HOL/Library/DAList.thy	Thu Feb 16 22:18:28 2012 +0100
     1.2 +++ b/src/HOL/Library/DAList.thy	Thu Feb 16 22:53:24 2012 +0100
     1.3 @@ -12,8 +12,10 @@
     1.4  subsection {* Type @{text "('key, 'value) alist" } *}
     1.5  
     1.6  typedef (open) ('key, 'value) alist = "{xs :: ('key \<times> 'value) list. distinct (map fst xs)}"
     1.7 -morphisms impl_of Alist
     1.8 -by(rule exI[where x="[]"]) simp
     1.9 +  morphisms impl_of Alist
    1.10 +proof
    1.11 +  show "[] \<in> {xs. distinct (map fst xs)}" by simp
    1.12 +qed
    1.13  
    1.14  lemma alist_ext: "impl_of xs = impl_of ys \<Longrightarrow> xs = ys"
    1.15  by(simp add: impl_of_inject)