src/Doc/Tutorial/Misc/case_exprs.thy

--- a/src/Doc/Tutorial/Misc/case_exprs.thy	Sat Nov 01 11:40:55 2014 +0100
+++ b/src/Doc/Tutorial/Misc/case_exprs.thy	Sat Nov 01 14:20:38 2014 +0100
@@ -52,8 +52,8 @@
 by \methdx{case_tac}.  Here is a trivial example:
 *}
 
-lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs";
-apply(case_tac xs);
+lemma "(case xs of [] \<Rightarrow> [] | y#ys \<Rightarrow> xs) = xs"
+apply(case_tac xs)
 
 txt{*\noindent
 results in the proof state