src/HOL/Library/Countable.thy
changeset 39250 548a3e5521ab
parent 39198 f967a16dfcdd
child 39302 d7728f65b353
equal deleted inserted replaced
39249:9c866b248cb1 39250:548a3e5521ab
    98 
    98 
    99 
    99 
   100 text {* Further *}
   100 text {* Further *}
   101 
   101 
   102 instance String.literal :: countable
   102 instance String.literal :: countable
   103   by (rule countable_classI [of "String.literal_case to_nat"])
   103   by (rule countable_classI [of "to_nat o explode"])
   104    (auto split: String.literal.splits)
   104     (auto simp add: explode_inject)
   105 
   105 
   106 instantiation typerep :: countable
   106 instantiation typerep :: countable
   107 begin
   107 begin
   108 
   108 
   109 fun to_nat_typerep :: "typerep \<Rightarrow> nat" where
   109 fun to_nat_typerep :: "typerep \<Rightarrow> nat" where