| changeset 31718 | 7715d4d3586f |
| parent 31148 | 7ba7c1f8bc22 |
| child 33318 | ddd97d9dfbfb |
--- 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]