--- a/src/Doc/Isar_Ref/Proof_Script.thy Sun Feb 07 14:36:16 2016 +0100
+++ b/src/Doc/Isar_Ref/Proof_Script.thy Sun Feb 07 19:32:35 2016 +0100
@@ -13,10 +13,13 @@
Nonetheless, it is possible to emulate proof scripts by sequential
refinements of a proof state in backwards mode, notably with the @{command
- apply} command (see \secref{sec:tactic-commands}). There are also various
- proof methods that allow to refer to implicit goal state information that is
- normally not accessible to structured Isar proofs (see
- \secref{sec:tactics}).
+ apply} command (see \secref{sec:tactic-commands}).
+
+ There are also various proof methods that allow to refer to implicit goal
+ state information that is not accessible to structured Isar proofs (see
+ \secref{sec:tactics}). Note that the @{command subgoal}
+ (\secref{sec:subgoal}) command usually eliminates the need for implicit goal
+ state references.
\<close>
@@ -82,7 +85,7 @@
\<close>
-section \<open>Explicit subgoal structure\<close>
+section \<open>Explicit subgoal structure \label{sec:subgoal}\<close>
text \<open>
\begin{matharray}{rcl}