# HG changeset patch
# User krauss
# Date 1184613376 -7200
# Node ID ee3ee9ea0d34a008ce84128e8b2400dbe672fdff
# Parent  3879cb3d0ba7c5abdcbb966d17403d01b26c6e63
updated

diff -r 3879cb3d0ba7 -r ee3ee9ea0d34 src/HOL/ex/Fundefs.thy
--- a/src/HOL/ex/Fundefs.thy	Mon Jul 16 19:18:23 2007 +0200
+++ b/src/HOL/ex/Fundefs.thy	Mon Jul 16 21:16:16 2007 +0200
@@ -169,7 +169,7 @@
 thm evn.simps
 thm od.simps
 
-thm evn_od.pinduct
+thm evn_od.induct
 thm evn_od.termination