src/Doc/Isar_Ref/Proof_Script.thy
changeset 62269 c56cff1c0e73
parent 61866 6fa60a4f7e48
child 62271 4cfe65cfd369
     1.1 --- a/src/Doc/Isar_Ref/Proof_Script.thy	Sun Feb 07 14:36:16 2016 +0100
     1.2 +++ b/src/Doc/Isar_Ref/Proof_Script.thy	Sun Feb 07 19:32:35 2016 +0100
     1.3 @@ -13,10 +13,13 @@
     1.4  
     1.5    Nonetheless, it is possible to emulate proof scripts by sequential
     1.6    refinements of a proof state in backwards mode, notably with the @{command
     1.7 -  apply} command (see \secref{sec:tactic-commands}). There are also various
     1.8 -  proof methods that allow to refer to implicit goal state information that is
     1.9 -  normally not accessible to structured Isar proofs (see
    1.10 -  \secref{sec:tactics}).
    1.11 +  apply} command (see \secref{sec:tactic-commands}).
    1.12 +
    1.13 +  There are also various proof methods that allow to refer to implicit goal
    1.14 +  state information that is not accessible to structured Isar proofs (see
    1.15 +  \secref{sec:tactics}). Note that the @{command subgoal}
    1.16 +  (\secref{sec:subgoal}) command usually eliminates the need for implicit goal
    1.17 +  state references.
    1.18  \<close>
    1.19  
    1.20  
    1.21 @@ -82,7 +85,7 @@
    1.22  \<close>
    1.23  
    1.24  
    1.25 -section \<open>Explicit subgoal structure\<close>
    1.26 +section \<open>Explicit subgoal structure \label{sec:subgoal}\<close>
    1.27  
    1.28  text \<open>
    1.29    \begin{matharray}{rcl}