1.1 --- a/src/HOL/Library/Countable.thy	Wed Feb 24 14:42:28 2010 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Fri Feb 26 09:20:18 2010 +0100
     1.3 @@ -5,12 +5,7 @@
     1.4  header {* Encoding (almost) everything into natural numbers *}
     1.5  
     1.6  theory Countable
     1.7 -imports
     1.8 -  "~~/src/HOL/List"
     1.9 -  "~~/src/HOL/Hilbert_Choice"
    1.10 -  "~~/src/HOL/Nat_Int_Bij"
    1.11 -  "~~/src/HOL/Rational"
    1.12 -  Main
    1.13 +imports Main Rat Nat_Int_Bij
    1.14  begin
    1.15  
    1.16  subsection {* The class of countable types *}
    1.17 @@ -213,8 +208,8 @@
    1.18  proof
    1.19    fix r::rat
    1.20    show "\<exists>n. r = nat_to_rat_surj n"
    1.21 -  proof(cases r)
    1.22 -    fix i j assume [simp]: "r = Fract i j" and "j \<noteq> 0"
    1.23 +  proof (cases r)
    1.24 +    fix i j assume [simp]: "r = Fract i j" and "j > 0"
    1.25      have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j
    1.26                 in nat_to_rat_surj(nat2_to_nat (m,n)))"
    1.27        using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij]