--- a/src/ZF/Constructible/Normal.thy Tue Nov 07 19:39:54 2006 +0100
+++ b/src/ZF/Constructible/Normal.thy Tue Nov 07 19:40:13 2006 +0100
@@ -18,7 +18,7 @@
subsection {*Closed and Unbounded (c.u.) Classes of Ordinals*}
-constdefs
+definition
Closed :: "(i=>o) => o"
"Closed(P) == \<forall>I. I \<noteq> 0 --> (\<forall>i\<in>I. Ord(i) \<and> P(i)) --> P(\<Union>(I))"
@@ -200,7 +200,7 @@
subsection {*Normal Functions*}
-constdefs
+definition
mono_le_subset :: "(i=>i) => o"
"mono_le_subset(M) == \<forall>i j. i\<le>j --> M(i) \<subseteq> M(j)"
@@ -372,7 +372,7 @@
only if @{text F} is continuous: succ is not bounded above by any
normal function, by @{thm [source] Normal_imp_fp_Unbounded}.
*}
-constdefs
+definition
normalize :: "[i=>i, i] => i"
"normalize(F,a) == transrec2(a, F(0), \<lambda>x r. F(succ(x)) Un succ(r))"
@@ -424,12 +424,12 @@
text {*This is the well-known transfinite enumeration of the cardinal
numbers.*}
-constdefs
+definition
Aleph :: "i => i"
"Aleph(a) == transrec2(a, nat, \<lambda>x r. csucc(r))"
-syntax (xsymbols)
- Aleph :: "i => i" ("\<aleph>_" [90] 90)
+notation (xsymbols)
+ Aleph ("\<aleph>_" [90] 90)
lemma Card_Aleph [simp, intro]:
"Ord(a) ==> Card(Aleph(a))"
@@ -458,4 +458,3 @@
done
end
-