--- a/doc-src/TutorialI/Overview/LNCS/Ordinal.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/doc-src/TutorialI/Overview/LNCS/Ordinal.thy Mon Mar 01 13:40:23 2010 +0100
@@ -9,8 +9,7 @@
"pred (Succ a) n = Some a"
"pred (Limit f) n = Some (f n)"
-constdefs
- OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
+definition OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" where
"OpLim F a \<equiv> Limit (\<lambda>n. F n a)"
OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" ("\<Squnion>")
"\<Squnion>f \<equiv> OpLim (power f)"
@@ -29,8 +28,7 @@
"\<nabla>f (Succ a) = f (Succ (\<nabla>f a))"
"\<nabla>f (Limit h) = Limit (\<lambda>n. \<nabla>f (h n))"
-constdefs
- deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
+definition deriv :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)" where
"deriv f \<equiv> \<nabla>(\<Squnion>f)"
consts
@@ -40,8 +38,7 @@
"veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))"
"veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
-constdefs
- veb :: "ordinal \<Rightarrow> ordinal"
+definition veb :: "ordinal \<Rightarrow> ordinal" where
"veb a \<equiv> veblen a Zero"
epsilon0 :: ordinal ("\<epsilon>\<^sub>0")
"\<epsilon>\<^sub>0 \<equiv> veb Zero"