changeset 2469 | b50b8c0eec01 |
parent 1478 | 2b8c2a7547ab |
child 2539 | ddd22ceee8cc |
--- a/src/ZF/Ordinal.thy Fri Jan 03 10:48:28 1997 +0100 +++ b/src/ZF/Ordinal.thy Fri Jan 03 15:01:55 1997 +0100 @@ -6,7 +6,7 @@ Ordinals in Zermelo-Fraenkel Set Theory *) -Ordinal = WF + Bool + "simpdata" + "equalities" + +Ordinal = WF + Bool + equalities + consts Memrel :: i=>i Transset,Ord :: i=>o