# HG changeset patch
# User hoelzl
# Date 1311079069 -7200
# Node ID c6f35921056eb0325d9417ac3150fe130561a6ed
# Parent  e8511be08dddf25ecb46ba090655712e0490394c
add nat => enat coercion

diff -r e8511be08ddd -r c6f35921056e src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:37:09 2011 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Tue Jul 19 14:37:49 2011 +0200
@@ -47,7 +47,8 @@
   qed
 qed (auto simp add: Fin_def infinity_enat_def Abs_enat_inject)
 
-declare [[coercion "Fin :: nat \<Rightarrow> enat"]]
+declare [[coercion_enabled]]
+declare [[coercion "Fin::nat\<Rightarrow>enat"]]
 
 lemma not_Infty_eq[iff]: "(x \<noteq> \<infinity>) = (EX i. x = Fin i)"
 by (cases x) auto