# HG changeset patch
# User nipkow
# Date 1245427269 -7200
# Node ID 7715d4d3586f7083bb0c133542d62f2961e65b09
# Parent  d1f7b6245a754ea508d47ea284b46c4cd3de5b45
fixed thm name

diff -r d1f7b6245a75 -r 7715d4d3586f src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Thu Jun 18 18:31:14 2009 -0700
+++ b/src/HOL/Parity.thy	Fri Jun 19 18:01:09 2009 +0200
@@ -35,7 +35,7 @@
 
 lemma even_zero_nat[simp]: "even (0::nat)" by presburger
 
-lemma odd_zero_nat [simp]: "odd (1::nat)" by presburger
+lemma odd_1_nat [simp]: "odd (1::nat)" by presburger
 
 declare even_def[of "number_of v", standard, simp]