diff -r a0460a450cf9 -r bbfc360db011 doc-src/TutorialI/Overview/Ordinal.thy
--- a/doc-src/TutorialI/Overview/Ordinal.thy	Mon Jul 01 12:50:35 2002 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,52 +0,0 @@
-theory Ordinal = Main:
-
-datatype ordinal = Zero | Succ ordinal | Limit "nat \<Rightarrow> ordinal"
-
-consts
-  pred :: "ordinal \<Rightarrow> nat \<Rightarrow> ordinal option"
-primrec
-  "pred Zero n = None"
-  "pred (Succ a) n = Some a"
-  "pred (Limit f) n = Some (f n)"
-
-constdefs
-  OpLim :: "(nat \<Rightarrow> (ordinal \<Rightarrow> ordinal)) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"
-  "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)"
-
-consts
-  cantor :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
-primrec
-  "cantor a Zero = Succ a"
-  "cantor a (Succ b) = \<Squnion>(\<lambda>x. cantor x b) a"
-  "cantor a (Limit f) = Limit (\<lambda>n. cantor a (f n))"
-
-consts
-  Nabla :: "(ordinal \<Rightarrow> ordinal) \<Rightarrow> (ordinal \<Rightarrow> ordinal)"    ("\<nabla>")
-primrec
-  "\<nabla>f Zero = f Zero"
-  "\<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)"
-  "deriv f \<equiv> \<nabla>(\<Squnion>f)"
-
-consts
-  veblen :: "ordinal \<Rightarrow> ordinal \<Rightarrow> ordinal"
-primrec
-  "veblen Zero = \<nabla>(OpLim (power (cantor Zero)))"
-  "veblen (Succ a) = \<nabla>(OpLim (power (veblen a)))"
-  "veblen (Limit f) = \<nabla>(OpLim (\<lambda>n. veblen (f n)))"
-
-constdefs
-  veb :: "ordinal \<Rightarrow> ordinal"
-  "veb a \<equiv> veblen a Zero"
-  epsilon0 :: ordinal    ("\<epsilon>\<^sub>0")
-  "\<epsilon>\<^sub>0 \<equiv> veb Zero"
-  Gamma0 :: ordinal    ("\<Gamma>\<^sub>0")
-  "\<Gamma>\<^sub>0 \<equiv> Limit (\<lambda>n. (veb^n) Zero)"
-thm Gamma0_def
-
-end