src/HOL/Library/Countable.thy
changeset 39250 548a3e5521ab
parent 39198 f967a16dfcdd
child 39302 d7728f65b353
     1.1 --- a/src/HOL/Library/Countable.thy	Thu Sep 09 11:10:44 2010 +0200
     1.2 +++ b/src/HOL/Library/Countable.thy	Thu Sep 09 14:38:14 2010 +0200
     1.3 @@ -100,8 +100,8 @@
     1.4  text {* Further *}
     1.5  
     1.6  instance String.literal :: countable
     1.7 -  by (rule countable_classI [of "String.literal_case to_nat"])
     1.8 -   (auto split: String.literal.splits)
     1.9 +  by (rule countable_classI [of "to_nat o explode"])
    1.10 +    (auto simp add: explode_inject)
    1.11  
    1.12  instantiation typerep :: countable
    1.13  begin