# HG changeset patch
# User wenzelm
# Date 1213108987 -7200
# Node ID 56617a7b68c58c58b40890427e30d032e102dc91
# Parent  0dcafa5c9e3fc7bc4265989a7d0e690fecba832e
tuned;

diff -r 0dcafa5c9e3f -r 56617a7b68c5 doc-src/IsarRef/Thy/Proof.thy
--- a/doc-src/IsarRef/Thy/Proof.thy	Tue Jun 10 16:43:01 2008 +0200
+++ b/doc-src/IsarRef/Thy/Proof.thy	Tue Jun 10 16:43:07 2008 +0200
@@ -342,7 +342,7 @@
   meaning: (1) during the of this claim they refer to the the local
   context introductions, (2) the resulting rule is annotated
   accordingly to support symbolic case splits when used with the
-  @{method_ref cases} method (cf.  \secref{sec:cases-induct}).
+  @{method_ref cases} method (cf.\ \secref{sec:cases-induct}).
 
   \medskip