src/HOL/Library/Dlist.thy
changeset 49834 b27bbb021df1
parent 48282 39bfb2844b9e
child 55467 a5c9002bc54d
     1.1 --- a/src/HOL/Library/Dlist.thy	Fri Oct 12 15:08:29 2012 +0200
     1.2 +++ b/src/HOL/Library/Dlist.thy	Fri Oct 12 18:58:20 2012 +0200
     1.3 @@ -8,7 +8,7 @@
     1.4  
     1.5  subsection {* The type of distinct lists *}
     1.6  
     1.7 -typedef (open) 'a dlist = "{xs::'a list. distinct xs}"
     1.8 +typedef 'a dlist = "{xs::'a list. distinct xs}"
     1.9    morphisms list_of_dlist Abs_dlist
    1.10  proof
    1.11    show "[] \<in> {xs. distinct xs}" by simp