equal
deleted
inserted
replaced
4 Copyright 1994 University of Cambridge |
4 Copyright 1994 University of Cambridge |
5 |
5 |
6 Ordinals in Zermelo-Fraenkel Set Theory |
6 Ordinals in Zermelo-Fraenkel Set Theory |
7 *) |
7 *) |
8 |
8 |
9 Ordinal = WF + "simpdata" + "equalities" + |
9 Ordinal = WF + Bool + "simpdata" + "equalities" + |
10 consts |
10 consts |
11 Memrel :: "i=>i" |
11 Memrel :: "i=>i" |
12 Transset,Ord :: "i=>o" |
12 Transset,Ord :: "i=>o" |
13 "<" :: "[i,i] => o" (infixl 50) (*less than on ordinals*) |
13 "<" :: "[i,i] => o" (infixl 50) (*less than on ordinals*) |
14 "le" :: "[i,i] => o" (infixl 50) (*less than or equals*) |
14 "le" :: "[i,i] => o" (infixl 50) (*less than or equals*) |