src/HOL/Library/Extended_Nat.thy
changeset 43923 ab93d0190a5d
parent 43922 c6f35921056e
child 43924 1165fe965da8
     1.1 --- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:37:49 2011 +0200
     1.2 +++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:38:29 2011 +0200
     1.3 @@ -47,7 +47,6 @@
     1.4    qed
     1.5  qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
     1.6  
     1.7 -declare [[coercion_enabled]]
     1.8  declare [[coercion "Fin::nat\<Rightarrow>enat"]]
     1.9  
    1.10  lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"