changeset 19583 | c5fa77b03442 |
parent 19568 | 6fa47aad35e9 |
child 19736 | d8d0f8f51d69 |
--- a/src/HOL/ex/Fundefs.thy Fri May 05 22:11:19 2006 +0200 +++ b/src/HOL/ex/Fundefs.thy Sun May 07 00:00:13 2006 +0200 @@ -58,7 +58,7 @@ by pat_completeness auto lemma nz_is_zero: (* A lemma we need to prove termination *) - assumes trm: "x \<in> nz.dom" + assumes trm: "x \<in> nz_dom" shows "nz x = 0" using trm by induct auto