src/HOL/Library/Countable.thy
changeset 62087 44841d07ef1d
parent 61115 3a4400985780
child 62691 9bfcbab7cd99
     1.1 --- a/src/HOL/Library/Countable.thy	Wed Jan 06 16:17:50 2016 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Thu Jan 07 17:40:55 2016 +0000
     1.3 @@ -7,7 +7,7 @@
     1.4  section \<open>Encoding (almost) everything into natural numbers\<close>
     1.5  
     1.6  theory Countable
     1.7 -imports Old_Datatype Rat Nat_Bijection
     1.8 +imports Old_Datatype "~~/src/HOL/Rat" Nat_Bijection
     1.9  begin
    1.10  
    1.11  subsection \<open>The class of countable types\<close>