# HG changeset patch
# User wenzelm
# Date 1234815814 -3600
# Node ID 9c6c1b3f3eb6fd15b844afcf7e26e85562ac3e47
# Parent  bcb79ddf57da2da0de9ca375eefbd7c275b4f27d
tuned refs;

diff -r bcb79ddf57da -r 9c6c1b3f3eb6 doc-src/IsarImplementation/Thy/Proof.thy
--- a/doc-src/IsarImplementation/Thy/Proof.thy	Mon Feb 16 21:23:34 2009 +0100
+++ b/doc-src/IsarImplementation/Thy/Proof.thy	Mon Feb 16 21:23:34 2009 +0100
@@ -173,8 +173,7 @@
   rules.  Note that the discharged portion is determined by the
   difference contexts, not the facts being exported!  There is a
   separate flag to indicate a goal context, where the result is meant
-  to refine an enclosing sub-goal of a structured proof state (cf.\
-  \secref{sec:isar-proof-state}).
+  to refine an enclosing sub-goal of a structured proof state.
 
   \medskip The most basic export rule discharges assumptions directly
   by means of the @{text "\<Longrightarrow>"} introduction rule: