src/HOL/String.thy
changeset 49834 b27bbb021df1
parent 48891 c0eafbd55de3
child 49948 744934b818c7
     1.1 --- a/src/HOL/String.thy	Fri Oct 12 15:08:29 2012 +0200
     1.2 +++ b/src/HOL/String.thy	Fri Oct 12 18:58:20 2012 +0200
     1.3 @@ -152,7 +152,7 @@
     1.4  
     1.5  subsection {* Strings as dedicated type *}
     1.6  
     1.7 -typedef (open) literal = "UNIV :: string set"
     1.8 +typedef literal = "UNIV :: string set"
     1.9    morphisms explode STR ..
    1.10  
    1.11  instantiation literal :: size