--- a/src/ZF/Constructible/Rank.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Rank.thy Tue Nov 07 19:40:13 2006 +0100
@@ -136,7 +136,7 @@
done
-constdefs
+definition
obase :: "[i=>o,i,i] => i"
--{*the domain of @{text om}, eventually shown to equal @{text A}*}
@@ -414,7 +414,7 @@
subsubsection{*Ordinal Addition*}
(*FIXME: update to use new techniques!!*)
-constdefs
+definition
(*This expresses ordinal addition in the language of ZF. It also
provides an abbreviation that can be used in the instance of strong
replacement below. Here j is used to define the relation, namely
@@ -725,7 +725,7 @@
text{*This function, defined using replacement, is a rank function for
well-founded relations within the class M.*}
-constdefs
+definition
wellfoundedrank :: "[i=>o,i,i] => i"
"wellfoundedrank(M,r,A) ==
{p. x\<in>A, \<exists>y[M]. \<exists>f[M].