src/ZF/Nat.thy
 changeset 1478 2b8c2a7547ab parent 1401 0c439768f45c child 2469 b50b8c0eec01
```     1.1 --- a/src/ZF/Nat.thy	Mon Feb 05 21:33:14 1996 +0100
1.2 +++ b/src/ZF/Nat.thy	Tue Feb 06 12:27:17 1996 +0100
1.3 @@ -1,6 +1,6 @@
1.4 -(*  Title: 	ZF/Nat.thy
1.5 +(*  Title:      ZF/Nat.thy
1.6      ID:         \$Id\$
1.7 -    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
1.8 +    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
1.9      Copyright   1994  University of Cambridge
1.10
1.11  Natural numbers in Zermelo-Fraenkel Set Theory
1.12 @@ -8,7 +8,7 @@
1.13
1.14  Nat = Ordinal + Bool + "mono" +
1.15  consts
1.16 -    nat 	::      i
1.17 +    nat         ::      i
1.18      nat_case    ::      [i, i=>i, i]=>i
1.19      nat_rec     ::      [i, i, [i,i]=>i]=>i
1.20
1.21 @@ -17,10 +17,10 @@
1.22      nat_def     "nat == lfp(Inf, %X. {0} Un {succ(i). i:X})"
1.23
1.24      nat_case_def
1.25 -	"nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
1.26 +        "nat_case(a,b,k) == THE y. k=0 & y=a | (EX x. k=succ(x) & y=b(x))"
1.27
1.28      nat_rec_def
1.29 -	"nat_rec(k,a,b) ==
1.30 -   	  wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
1.31 +        "nat_rec(k,a,b) ==
1.32 +          wfrec(Memrel(nat), k, %n f. nat_case(a, %m. b(m, f`m), n))"
1.33
1.34  end
```