--- a/src/ZF/ex/Ntree.thy Thu May 31 17:57:02 2001 +0200 +++ b/src/ZF/ex/Ntree.thy Thu May 31 18:28:23 2001 +0200 @@ -9,7 +9,7 @@ Based upon ex/Term.thy *) -Ntree = InfDatatype + +Ntree = Main + consts ntree :: i=>i maptree :: i=>i