repaired definition (cf. d8d7d1b785af)

--- a/doc-src/TutorialI/Overview/LNCS/Ordinal.thy	Mon Mar 01 17:45:19 2010 +0100
+++ b/doc-src/TutorialI/Overview/LNCS/Ordinal.thy	Tue Mar 02 08:28:06 2010 +0100
@@ -11,7 +11,8 @@
 
 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>")
+
+definition OpItw :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"    ("\<Squnion>") where
   "\<Squnion>f \<equiv> OpLim (power f)"
 
 consts
@@ -40,9 +41,11 @@
 
 definition veb :: "ordinal \<Rightarrow> ordinal" where
   "veb a \<equiv> veblen a Zero"
-  epsilon0 :: ordinal    ("\<epsilon>\<^sub>0")
+
+definition epsilon0 :: ordinal    ("\<epsilon>\<^sub>0") where
   "\<epsilon>\<^sub>0 \<equiv> veb Zero"
-  Gamma0 :: ordinal    ("\<Gamma>\<^sub>0")
+
+definition Gamma0 :: ordinal    ("\<Gamma>\<^sub>0") where
   "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)"
 thm Gamma0_def