diff -r 4dc65845eab3 -r d8d7d1b785af doc-src/TutorialI/Overview/LNCS/Ordinal.thy
--- 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"