src/HOL/Nat.thy
changeset 39302 d7728f65b353
parent 39198 f967a16dfcdd
child 39793 4bd217def154
     1.1 --- a/src/HOL/Nat.thy	Mon Sep 13 08:43:48 2010 +0200
     1.2 +++ b/src/HOL/Nat.thy	Mon Sep 13 11:13:15 2010 +0200
     1.3 @@ -1360,7 +1360,7 @@
     1.4    by (induct n) simp_all
     1.5  
     1.6  lemma of_nat_eq_id [simp]: "of_nat = id"
     1.7 -  by (auto simp add: ext_iff)
     1.8 +  by (auto simp add: fun_eq_iff)
     1.9  
    1.10  
    1.11  subsection {* The Set of Natural Numbers *}