1.1 --- a/doc-src/IsarImplementation/Thy/Proof.thy	Fri Oct 15 20:22:56 2010 +0100
     1.2 +++ b/doc-src/IsarImplementation/Thy/Proof.thy	Fri Oct 15 20:36:52 2010 +0100
     1.3 @@ -397,6 +397,9 @@
     1.4    Proof.context -> int -> tactic"} \\
     1.5    @{index_ML Subgoal.FOCUS_PARAMS: "(Subgoal.focus -> tactic) ->
     1.6    Proof.context -> int -> tactic"} \\
     1.7 +  @{index_ML Subgoal.focus: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
     1.8 +  @{index_ML Subgoal.focus_prems: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
     1.9 +  @{index_ML Subgoal.focus_params: "Proof.context -> int -> thm -> Subgoal.focus * thm"} \\
    1.10    \end{mldecls}
    1.11  
    1.12    \begin{mldecls}
    1.13 @@ -424,6 +427,12 @@
    1.14    imported into the context, and the body tactic may introduce new
    1.15    subgoals and schematic variables.
    1.16  
    1.17 +  \item @{ML Subgoal.focus}, @{ML Subgoal.focus_prems}, @{ML
    1.18 +  Subgoal.focus_params} extract the focus information from a goal
    1.19 +  state in the same way as the corresponding tacticals above.  This is
    1.20 +  occasionally useful to experiment without writing actual tactics
    1.21 +  yet.
    1.22 +
    1.23    \item @{ML Goal.prove}~@{text "ctxt xs As C tac"} states goal @{text
    1.24    "C"} in the context augmented by fixed variables @{text "xs"} and
    1.25    assumptions @{text "As"}, and applies tactic @{text "tac"} to solve
    1.26 @@ -443,9 +452,25 @@
    1.27    \end{description}
    1.28  *}
    1.29  
    1.30 -text %mlex {* The following example demonstrates forward-elimination
    1.31 -  in a local context, using @{ML Obtain.result}.
    1.32 -*}
    1.33 +text %mlex {* The following minimal example illustrates how to access
    1.34 +  the focus information of a structured goal state. *}
    1.35 +
    1.36 +example_proof
    1.37 +  fix A B C :: "'a \<Rightarrow> bool"
    1.38 +
    1.39 +  have "\<And>x. A x \<Longrightarrow> B x \<Longrightarrow> C x"
    1.40 +    ML_val
    1.41 +    {*
    1.42 +      val {goal, context = goal_ctxt, ...} = @{Isar.goal};
    1.43 +      val (focus as {params, asms, concl, ...}, goal') =
    1.44 +        Subgoal.focus goal_ctxt 1 goal;
    1.45 +      val [A, B] = #prems focus;
    1.46 +      val [(_, x)] = #params focus;
    1.47 +    *}
    1.48 +    oops
    1.49 +
    1.50 +text {* \medskip The next example demonstrates forward-elimination in
    1.51 +  a local context, using @{ML Obtain.result}.  *}
    1.52  
    1.53  example_proof
    1.54    assume ex: "\<exists>x. B x"