--- a/src/HOL/ex/NatSum.thy Wed Nov 08 22:24:54 2006 +0100
+++ b/src/HOL/ex/NatSum.thy Wed Nov 08 23:11:13 2006 +0100
@@ -5,7 +5,7 @@
header {* Summing natural numbers *}
-theory NatSum imports Main begin
+theory NatSum imports Main Parity begin
text {*
Summing natural numbers, squares, cubes, etc.