equal
deleted
inserted
replaced
1 (* Title: ZF/nat.thy |
1 (* Title: ZF/Nat.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
3 Author: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 Copyright 1992 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Natural numbers in Zermelo-Fraenkel Set Theory |
6 Natural numbers in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 Nat = Ord + Bool + "mono" + |
9 Nat = Ordinal + Bool + "mono" + |
10 consts |
10 consts |
11 nat :: "i" |
11 nat :: "i" |
12 nat_case :: "[i, i=>i, i]=>i" |
12 nat_case :: "[i, i=>i, i]=>i" |
13 nat_rec :: "[i, i, [i,i]=>i]=>i" |
13 nat_rec :: "[i, i, [i,i]=>i]=>i" |
14 |
14 |