src/HOL/Library/Countable.thy
changeset 68028 1f9f973eed2a
parent 67405 e9ab4ad7bd15
child 68406 6beb45f6cf67
     1.1 --- a/src/HOL/Library/Countable.thy	Tue Apr 24 14:17:57 2018 +0000
     1.2 +++ b/src/HOL/Library/Countable.thy	Tue Apr 24 14:17:58 2018 +0000
     1.3 @@ -256,7 +256,7 @@
     1.4  text \<open>String literals\<close>
     1.5  
     1.6  instance String.literal :: countable
     1.7 -  by (rule countable_classI [of "to_nat \<circ> String.explode"]) (auto simp add: explode_inject)
     1.8 +  by (rule countable_classI [of "to_nat \<circ> String.explode"]) (simp add: String.explode_inject)
     1.9  
    1.10  text \<open>Functions\<close>
    1.11