# HG changeset patch
# User wenzelm
# Date 1352300563 -3600
# Node ID 775445d65e17ca17623fcc6c7d71851e6fa1bee4
# Parent  959548c3b9476d739c755f20aaa1b91a65898889
updated biresolve_tac, bimatch_tac;
removed obscure historical material;

diff -r 959548c3b947 -r 775445d65e17 src/Doc/IsarImplementation/Tactic.thy
--- a/src/Doc/IsarImplementation/Tactic.thy	Wed Nov 07 12:14:38 2012 +0100
+++ b/src/Doc/IsarImplementation/Tactic.thy	Wed Nov 07 16:02:43 2012 +0100
@@ -265,12 +265,14 @@
   @{index_ML resolve_tac: "thm list -> int -> tactic"} \\
   @{index_ML eresolve_tac: "thm list -> int -> tactic"} \\
   @{index_ML dresolve_tac: "thm list -> int -> tactic"} \\
-  @{index_ML forward_tac: "thm list -> int -> tactic"} \\[1ex]
+  @{index_ML forward_tac: "thm list -> int -> tactic"} \\
+  @{index_ML biresolve_tac: "(bool * thm) list -> int -> tactic"} \\[1ex]
   @{index_ML assume_tac: "int -> tactic"} \\
   @{index_ML eq_assume_tac: "int -> tactic"} \\[1ex]
   @{index_ML match_tac: "thm list -> int -> tactic"} \\
   @{index_ML ematch_tac: "thm list -> int -> tactic"} \\
   @{index_ML dmatch_tac: "thm list -> int -> tactic"} \\
+  @{index_ML bimatch_tac: "(bool * thm) list -> int -> tactic"} \\
   \end{mldecls}
 
   \begin{description}
@@ -297,6 +299,16 @@
   selected assumption is not deleted.  It applies a rule to an
   assumption, adding the result as a new assumption.
 
+  \item @{ML biresolve_tac}~@{text "brls i"} refines the proof state
+  by resolution or elim-resolution on each rule, as indicated by its
+  flag.  It affects subgoal @{text "i"} of the proof state.
+
+  For each pair @{text "(flag, rule)"}, it applies resolution if the
+  flag is @{text "false"} and elim-resolution if the flag is @{text
+  "true"}.  A single tactic call handles a mixture of introduction and
+  elimination rules, which is useful to organize the search process
+  systematically in proof tools.
+
   \item @{ML assume_tac}~@{text i} attempts to solve subgoal @{text i}
   by assumption (modulo higher-order unification).
 
@@ -306,10 +318,10 @@
   assumptions is equal to the subgoal's conclusion.  Since it does not
   instantiate variables, it cannot make other subgoals unprovable.
 
-  \item @{ML match_tac}, @{ML ematch_tac}, and @{ML dmatch_tac} are
-  similar to @{ML resolve_tac}, @{ML eresolve_tac}, and @{ML
-  dresolve_tac}, respectively, but do not instantiate schematic
-  variables in the goal state.
+  \item @{ML match_tac}, @{ML ematch_tac}, @{ML dmatch_tac}, and @{ML
+  bimatch_tac} are similar to @{ML resolve_tac}, @{ML eresolve_tac},
+  @{ML dresolve_tac}, and @{ML biresolve_tac}, respectively, but do
+  not instantiate schematic variables in the goal state.
 
   Flexible subgoals are not updated at will, but are left alone.
   Strictly speaking, matching means to treat the unknowns in the goal
diff -r 959548c3b947 -r 775445d65e17 src/Doc/Ref/document/tactic.tex
--- a/src/Doc/Ref/document/tactic.tex	Wed Nov 07 12:14:38 2012 +0100
+++ b/src/Doc/Ref/document/tactic.tex	Wed Nov 07 16:02:43 2012 +0100
@@ -4,25 +4,6 @@
 
 \section{Other basic tactics}
 
-\subsection{Inserting premises and facts}\label{cut_facts_tac}
-\index{tactics!for inserting facts}\index{assumptions!inserting}
-\begin{ttbox} 
-cut_facts_tac : thm list -> int -> tactic
-\end{ttbox}
-These tactics add assumptions to a subgoal.
-\begin{ttdescription}
-\item[\ttindexbold{cut_facts_tac} {\it thms} {\it i}] 
-  adds the {\it thms} as new assumptions to subgoal~$i$.  Once they have
-  been inserted as assumptions, they become subject to tactics such as {\tt
-    eresolve_tac} and {\tt rewrite_goals_tac}.  Only rules with no premises
-  are inserted: Isabelle cannot use assumptions that contain $\Imp$
-  or~$\Forall$.  Sometimes the theorems are premises of a rule being
-  derived, returned by~{\tt goal}; instead of calling this tactic, you
-  could state the goal with an outermost meta-quantifier.
-
-\end{ttdescription}
-
-
 \subsection{Composition: resolution without lifting}
 \index{tactics!for composition}
 \begin{ttbox}
@@ -51,45 +32,6 @@
 resolution, and can also detect whether a subgoal is too flexible,
 with too many rules applicable.
 
-\subsection{Combined resolution and elim-resolution} \label{biresolve_tac}
-\index{tactics!resolution}
-\begin{ttbox} 
-biresolve_tac   : (bool*thm)list -> int -> tactic
-bimatch_tac     : (bool*thm)list -> int -> tactic
-subgoals_of_brl : bool*thm -> int
-lessb           : (bool*thm) * (bool*thm) -> bool
-\end{ttbox}
-{\bf Bi-resolution} takes a list of $\it (flag,rule)$ pairs.  For each
-pair, it applies resolution if the flag is~{\tt false} and
-elim-resolution if the flag is~{\tt true}.  A single tactic call handles a
-mixture of introduction and elimination rules.
-
-\begin{ttdescription}
-\item[\ttindexbold{biresolve_tac} {\it brls} {\it i}] 
-refines the proof state by resolution or elim-resolution on each rule, as
-indicated by its flag.  It affects subgoal~$i$ of the proof state.
-
-\item[\ttindexbold{bimatch_tac}] 
-is like {\tt biresolve_tac}, but performs matching: unknowns in the
-proof state are never updated (see~{\S}\ref{match_tac}).
-
-\item[\ttindexbold{subgoals_of_brl}({\it flag},{\it rule})] 
-returns the number of new subgoals that bi-res\-o\-lu\-tion would yield for the
-pair (if applied to a suitable subgoal).  This is $n$ if the flag is
-{\tt false} and $n-1$ if the flag is {\tt true}, where $n$ is the number
-of premises of the rule.  Elim-resolution yields one fewer subgoal than
-ordinary resolution because it solves the major premise by assumption.
-
-\item[\ttindexbold{lessb} ({\it brl1},{\it brl2})] 
-returns the result of 
-\begin{ttbox}
-subgoals_of_brl{\it brl1} < subgoals_of_brl{\it brl2}
-\end{ttbox}
-\end{ttdescription}
-Note that \hbox{\tt sort lessb {\it brls}} sorts a list of $\it
-(flag,rule)$ pairs by the number of new subgoals they will yield.  Thus,
-those that yield the fewest subgoals should be tried first.
-
 
 \subsection{Discrimination nets for fast resolution}\label{filt_resolve_tac}
 \index{discrimination nets|bold}