# HG changeset patch
# User haftmann
# Date 1267172418 -3600
# Node ID af1c8c15340e237b24fec114ffdb023dc1990cc2
# Parent  f759782e35ac1a5fea6f1eae6003e7e055e8ef98
adjusted to cs. e4a7947e02b8

diff -r f759782e35ac -r af1c8c15340e src/HOL/Library/Countable.thy
--- a/src/HOL/Library/Countable.thy	Wed Feb 24 14:42:28 2010 +0100
+++ b/src/HOL/Library/Countable.thy	Fri Feb 26 09:20:18 2010 +0100
@@ -5,12 +5,7 @@
 header {* Encoding (almost) everything into natural numbers *}
 
 theory Countable
-imports
-  "~~/src/HOL/List"
-  "~~/src/HOL/Hilbert_Choice"
-  "~~/src/HOL/Nat_Int_Bij"
-  "~~/src/HOL/Rational"
-  Main
+imports Main Rat Nat_Int_Bij
 begin
 
 subsection {* The class of countable types *}
@@ -213,8 +208,8 @@
 proof
   fix r::rat
   show "\<exists>n. r = nat_to_rat_surj n"
-  proof(cases r)
-    fix i j assume [simp]: "r = Fract i j" and "j \<noteq> 0"
+  proof (cases r)
+    fix i j assume [simp]: "r = Fract i j" and "j > 0"
     have "r = (let m = inv nat_to_int_bij i; n = inv nat_to_int_bij j
                in nat_to_rat_surj(nat2_to_nat (m,n)))"
       using nat2_to_nat_inj surj_f_inv_f[OF surj_nat_to_int_bij]