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