src/HOL/String.thy
changeset 57247 8191ccf6a1bd
parent 56846 9df717fef2bb
child 57437 0baf08c075b9
     1.1 --- a/src/HOL/String.thy	Thu Jun 12 15:47:36 2014 +0200
     1.2 +++ b/src/HOL/String.thy	Thu Jun 12 18:47:16 2014 +0200
     1.3 @@ -224,7 +224,7 @@
     1.4  
     1.5  instance proof
     1.6    show UNIV: "UNIV = set (Enum.enum :: char list)"
     1.7 -    by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
     1.8 +    by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
     1.9    show "distinct (Enum.enum :: char list)"
    1.10      by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
    1.11    show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"