changeset 29234 | 60f7fb56f8cd |
parent 23775 | 8b37b6615c52 |
child 44603 | a6f9a70d655d |
--- a/src/HOL/ex/Abstract_NAT.thy Sun Dec 14 18:45:51 2008 +0100 +++ b/src/HOL/ex/Abstract_NAT.thy Mon Dec 15 18:12:52 2008 +0100 @@ -1,5 +1,4 @@ (* - ID: $Id$ Author: Makarius *) @@ -131,7 +130,7 @@ text {* \medskip Just see that our abstract specification makes sense \dots *} -interpretation NAT [0 Suc] +interpretation NAT 0 Suc proof (rule NAT.intro) fix m n show "(Suc m = Suc n) = (m = n)" by simp