--- a/src/ZF/Nat.thy Mon Nov 28 19:48:30 1994 +0100
+++ b/src/ZF/Nat.thy Tue Nov 29 00:31:31 1994 +0100
@@ -12,7 +12,7 @@
nat_case :: "[i, i=>i, i]=>i"
nat_rec :: "[i, i, [i,i]=>i]=>i"
-rules
+defs
nat_def "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"