diff -r d5ff8b782b29 -r fee7cfa69c50 src/Doc/Tutorial/Misc/Tree.thy
--- a/src/Doc/Tutorial/Misc/Tree.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/Tree.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -6,25 +6,25 @@
 Define the datatype of \rmindex{binary trees}:
 *}
 
-datatype 'a tree = Tip | Node "'a tree" 'a "'a tree";(*<*)
+datatype 'a tree = Tip | Node "'a tree" 'a "'a tree"(*<*)
 
 primrec mirror :: "'a tree \<Rightarrow> 'a tree" where
 "mirror Tip = Tip" |
-"mirror (Node l x r) = Node (mirror r) x (mirror l)";(*>*)
+"mirror (Node l x r) = Node (mirror r) x (mirror l)"(*>*)
 
 text{*\noindent
 Define a function @{term"mirror"} that mirrors a binary tree
 by swapping subtrees recursively. Prove
 *}
 
-lemma mirror_mirror: "mirror(mirror t) = t";
+lemma mirror_mirror: "mirror(mirror t) = t"
 (*<*)
-apply(induct_tac t);
-by(auto);
+apply(induct_tac t)
+by(auto)
 
 primrec flatten :: "'a tree => 'a list" where
 "flatten Tip = []" |
-"flatten (Node l x r) = flatten l @ [x] @ flatten r";
+"flatten (Node l x r) = flatten l @ [x] @ flatten r"
 (*>*)
 
 text{*\noindent
@@ -32,10 +32,10 @@
 by traversing it in infix order. Prove
 *}
 
-lemma "flatten(mirror t) = rev(flatten t)";
+lemma "flatten(mirror t) = rev(flatten t)"
 (*<*)
-apply(induct_tac t);
-by(auto);
+apply(induct_tac t)
+by(auto)
 
 end
 (*>*)