updated documentation;
authorwenzelm
Thu Jun 27 10:35:37 2013 +0200 (2013-06-27)
changeset 52463c45a6939217f
parent 52462 a241826ed003
child 52464 36497ee02ed8
updated documentation;
NEWS
src/Doc/IsarImplementation/Proof.thy
src/Doc/IsarImplementation/Tactic.thy
     1.1 --- a/NEWS	Thu Jun 27 10:14:17 2013 +0200
     1.2 +++ b/NEWS	Thu Jun 27 10:35:37 2013 +0200
     1.3 @@ -68,6 +68,10 @@
     1.4  * Discontinued empty name bindings in 'axiomatization'.
     1.5  INCOMPATIBILITY.
     1.6  
     1.7 +* SELECT_GOAL now retains the syntactic context of the overall goal
     1.8 +state (schematic variables etc.).  Potential INCOMPATIBILITY in rare
     1.9 +situations.
    1.10 +
    1.11  
    1.12  *** HOL ***
    1.13  
     2.1 --- a/src/Doc/IsarImplementation/Proof.thy	Thu Jun 27 10:14:17 2013 +0200
     2.2 +++ b/src/Doc/IsarImplementation/Proof.thy	Thu Jun 27 10:35:37 2013 +0200
     2.3 @@ -387,7 +387,6 @@
     2.4  
     2.5  text %mlref {*
     2.6    \begin{mldecls}
     2.7 -  @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
     2.8    @{index_ML SUBPROOF: "(Subgoal.focus -> tactic) ->
     2.9    Proof.context -> int -> tactic"} \\
    2.10    @{index_ML Subgoal.FOCUS: "(Subgoal.focus -> tactic) ->
    2.11 @@ -414,10 +413,6 @@
    2.12  
    2.13    \begin{description}
    2.14  
    2.15 -  \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
    2.16 -  specified subgoal @{text "i"}.  This introduces a nested goal state,
    2.17 -  without decomposing the internal structure of the subgoal yet.
    2.18 -
    2.19    \item @{ML SUBPROOF}~@{text "tac ctxt i"} decomposes the structure
    2.20    of the specified sub-goal, producing an extended context and a
    2.21    reduced goal, which needs to be solved by the given tactic.  All
     3.1 --- a/src/Doc/IsarImplementation/Tactic.thy	Thu Jun 27 10:14:17 2013 +0200
     3.2 +++ b/src/Doc/IsarImplementation/Tactic.thy	Thu Jun 27 10:35:37 2013 +0200
     3.3 @@ -179,6 +179,8 @@
     3.4    @{index_ML PRIMITIVE: "(thm -> thm) -> tactic"} \\[1ex]
     3.5    @{index_ML SUBGOAL: "(term * int -> tactic) -> int -> tactic"} \\
     3.6    @{index_ML CSUBGOAL: "(cterm * int -> tactic) -> int -> tactic"} \\
     3.7 +  @{index_ML SELECT_GOAL: "tactic -> int -> tactic"} \\
     3.8 +  @{index_ML PREFER_GOAL: "tactic -> int -> tactic"} \\
     3.9    \end{mldecls}
    3.10  
    3.11    \begin{description}
    3.12 @@ -218,6 +220,16 @@
    3.13    avoids expensive re-certification in situations where the subgoal is
    3.14    used directly for primitive inferences.
    3.15  
    3.16 +  \item @{ML SELECT_GOAL}~@{text "tac i"} confines a tactic to the
    3.17 +  specified subgoal @{text "i"}.  This rearranges subgoals and the
    3.18 +  main goal protection (\secref{sec:tactical-goals}), while retaining
    3.19 +  the syntactic context of the overall goal state (concerning
    3.20 +  schematic variables etc.).
    3.21 +
    3.22 +  \item @{ML PREFER_GOAL}~@{text "tac i"} rearranges subgoals to put
    3.23 +  @{text "i"} in front.  This is similar to @{ML SELECT_GOAL}, but
    3.24 +  without changing the main goal protection.
    3.25 +
    3.26    \end{description}
    3.27  *}
    3.28