author | hoelzl |
Tue, 19 Jul 2011 14:37:49 +0200 | |
changeset 43922 | c6f35921056e |
parent 43921 | e8511be08ddd |
child 43923 | ab93d0190a5d |
--- 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