| changeset 21404 | eb85850d3eb7 |
| parent 19736 | d8d0f8f51d69 |
| child 23394 | 474ff28210c0 |
--- a/src/HOL/Library/NatPair.thy Fri Nov 17 02:19:55 2006 +0100 +++ b/src/HOL/Library/NatPair.thy Fri Nov 17 02:20:03 2006 +0100 @@ -16,7 +16,7 @@ *} definition - nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" + nat2_to_nat:: "(nat * nat) \<Rightarrow> nat" where "nat2_to_nat pair = (let (n,m) = pair in (n+m) * Suc (n+m) div 2 + n)" lemma dvd2_a_x_suc_a: "2 dvd a * (Suc a)"