diff -r 71b2a1fefb84 -r 3dc292be0b54 doc-src/TutorialI/Fun/fun0.thy
--- a/doc-src/TutorialI/Fun/fun0.thy	Fri Nov 02 08:26:01 2007 +0100
+++ b/doc-src/TutorialI/Fun/fun0.thy	Fri Nov 02 08:59:15 2007 +0100
@@ -88,9 +88,9 @@
 show that the size of one fixed argument becomes smaller with each
 recursive call.
 
-More generally, @{text fun} allows any \emph{lexicographic
+More generally, \isacommand{fun} allows any \emph{lexicographic
 combination} of size measures in case there are multiple
-arguments. For example the following version of \rmindex{Ackermann's
+arguments. For example, the following version of \rmindex{Ackermann's
 function} is accepted: *}
 
 fun ack2 :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
@@ -114,8 +114,8 @@
 Let us look at an example:
 *}
 
-fun gcd :: "nat \<times> nat \<Rightarrow> nat" where
-  "gcd(m,n) = (if n=0 then m else gcd(n, m mod n))"
+fun gcd :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
+  "gcd m n = (if n=0 then m else gcd n (m mod n))"
 
 text{*\noindent
 The second argument decreases with each recursive call.
@@ -130,12 +130,12 @@
 each @{text "if"}-expression unless its
 condition simplifies to @{term True} or @{term False}.  For
 example, simplification reduces
-@{prop[display]"gcd(m,n) = k"}
+@{prop[display]"gcd m n = k"}
 in one step to
-@{prop[display]"(if n=0 then m else gcd(n, m mod n)) = k"}
+@{prop[display]"(if n=0 then m else gcd n (m mod n)) = k"}
 where the condition cannot be reduced further, and splitting leads to
-@{prop[display]"(n=0 --> m=k) & (n ~= 0 --> gcd(n, m mod n)=k)"}
-Since the recursive call @{term"gcd(n, m mod n)"} is no longer protected by
+@{prop[display]"(n=0 --> m=k) & (n ~= 0 --> gcd n (m mod n)=k)"}
+Since the recursive call @{term"gcd n (m mod n)"} is no longer protected by
 an @{text "if"}, it is unfolded again, which leads to an infinite chain of
 simplification steps. Fortunately, this problem can be avoided in many
 different ways.
@@ -176,11 +176,11 @@
 these lemmas:
 *}
 
-lemma [simp]: "gcd(m,0) = m"
+lemma [simp]: "gcd m 0 = m"
 apply(simp)
 done
 
-lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd(m,n) = gcd(n, m mod n)"
+lemma [simp]: "n \<noteq> 0 \<Longrightarrow> gcd m n = gcd n (m mod n)"
 apply(simp)
 done