--- a/doc-src/TutorialI/Misc/Option2.thy Wed Feb 24 11:55:52 2010 +0100
+++ b/doc-src/TutorialI/Misc/Option2.thy Mon Mar 01 13:40:23 2010 +0100
@@ -24,8 +24,7 @@
*}
(*<*)
(*
-constdefs
- infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option"
+definition infplus :: "nat option \<Rightarrow> nat option \<Rightarrow> nat option" where
"infplus x y \<equiv> case x of None \<Rightarrow> None
| Some m \<Rightarrow> (case y of None \<Rightarrow> None | Some n \<Rightarrow> Some(m+n))"