# HG changeset patch
# User nipkow
# Date 1412330107 -7200
# Node ID ad010811f45053ea333b33fe58e9992058e3df16
# Parent  b70e93c05efee50d738ecba9182c441e4e3b1dd5
tuned

diff -r b70e93c05efe -r ad010811f450 src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Fri Oct 03 11:48:27 2014 +0200
+++ b/src/Doc/Prog_Prove/Isar.thy	Fri Oct 03 11:55:07 2014 +0200
@@ -863,7 +863,7 @@
 Because each \isacom{case} command introduces a list of assumptions
 named like the case name, which is the name of a rule of the inductive
 definition, those rules now need to be accessed with a qualified name, here
-@{thm[source] ev.ev0} and @{thm[source] ev.evSS}
+@{thm[source] ev.ev0} and @{thm[source] ev.evSS}.
 \end{warn}
 
 In the case @{thm[source]evSS} of the proof above we have pretended that the