# HG changeset patch
# User paulson
# Date 1376994906 -3600
# Node ID e79afad81386641da86c24e203423279112bb5c9
# Parent  7e89edba3db64dad93dadac77a9e64d45ffcfe49
Inserted footnote under match_tac

diff -r 7e89edba3db6 -r e79afad81386 src/Doc/IsarImplementation/Tactic.thy
--- a/src/Doc/IsarImplementation/Tactic.thy	Tue Aug 20 04:59:54 2013 +0200
+++ b/src/Doc/IsarImplementation/Tactic.thy	Tue Aug 20 11:35:06 2013 +0100
@@ -336,13 +336,15 @@
   \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.
+  not instantiate schematic variables in the goal state.%
+\footnote{Strictly speaking, matching means to treat the unknowns in the goal
+  state as constants, but these tactics merely discard unifiers that would
+  update the goal state. In rare situations (where the conclusion and 
+  goal state have flexible terms at the same position), the tactic
+  will fail even though an acceptable unifier exists.}
+  These tactics were written for a specific application within the classical reasoner.
 
   Flexible subgoals are not updated at will, but are left alone.
-  Strictly speaking, matching means to treat the unknowns in the goal
-  state as constants; these tactics merely discard unifiers that would
-  update the goal state.
-
   \end{description}
 *}