src/HOL/Library/Countable.thy
changeset 40702 cf26dd7395e4
parent 39302 d7728f65b353
child 43534 15df7bc8e93f
     1.1 --- a/src/HOL/Library/Countable.thy	Wed Nov 24 10:52:02 2010 +0100
     1.2 +++ b/src/HOL/Library/Countable.thy	Mon Nov 22 10:34:33 2010 +0100
     1.3 @@ -165,7 +165,7 @@
     1.4  qed
     1.5  
     1.6  lemma Rats_eq_range_nat_to_rat_surj: "\<rat> = range nat_to_rat_surj"
     1.7 -by (simp add: Rats_def surj_nat_to_rat_surj surj_range)
     1.8 +by (simp add: Rats_def surj_nat_to_rat_surj)
     1.9  
    1.10  context field_char_0
    1.11  begin