# HG changeset patch
# User lcp
# Date 789876100 -3600
# Node ID 664052e3cf66ede02e05479f72cb69760d4b0583
# Parent  f9172c4625f12bc0b814b9673790961def408f2c
Now depends upon Bool, so that 1 and 2 are defined

diff -r f9172c4625f1 -r 664052e3cf66 src/ZF/Ordinal.thy
--- a/src/ZF/Ordinal.thy	Thu Jan 12 03:01:20 1995 +0100
+++ b/src/ZF/Ordinal.thy	Thu Jan 12 03:01:40 1995 +0100
@@ -6,7 +6,7 @@
 Ordinals in Zermelo-Fraenkel Set Theory 
 *)
 
-Ordinal = WF + "simpdata" + "equalities" +
+Ordinal = WF + Bool + "simpdata" + "equalities" +
 consts
   Memrel      	:: "i=>i"
   Transset,Ord  :: "i=>o"