Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
Now depends upon Bool, so that 1 and 2 are defined
authorlcp
Thu, 12 Jan 1995 03:01:40 +0100
changeset 852 664052e3cf66
parent 851 f9172c4625f1
child 853 a4b286dfdd6f
Now depends upon Bool, so that 1 and 2 are defined
src/ZF/Ordinal.thy file | annotate | diff | comparison | revisions 
--- 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"
isabelle