--- a/src/ZF/ex/NatSum.thy Fri Jun 17 11:35:35 2005 +0200 +++ b/src/ZF/ex/NatSum.thy Fri Jun 17 16:12:49 2005 +0200 @@ -17,7 +17,7 @@ *) -theory NatSum = Main: +theory NatSum imports Main begin consts sum :: "[i=>i, i] => i" primrec