Method rule_tac understands Isar contexts: documentation.

--- a/NEWS	Fri Aug 29 15:19:02 2003 +0200
+++ b/NEWS	Fri Aug 29 15:40:11 2003 +0200
@@ -17,6 +17,22 @@
   symbols.  Call 'isatool fixgreek' to try to fix parsing errors in
   existing theory and ML files.
 
+*** Isar ***
+
+* Tactic emulation methods ?rule_tac, cut_tac, subgoal_tac and thin_tac:
+
+  - Now understand static (Isar) contexts.  As a consequence, users of Isar
+    locales are no longer forced to write Isar proof scripts.
+    For details see Isar Reference Manual, paragraph 4.3.2: Further tactic
+    emulations.
+  - INCOMPATIBILITY: names of variables to be instantiated may no
+    longer be enclosed in quotes.  Instead, precede variable names containing
+    dots with `?'.  This is consistent with the instantiation attribute
+    "where".
+
+* HOL: Tactic emulation methods induct_tac and case_tac understand static
+  (Isar) contexts.
+
 *** HOL ***
 
 * 'specification' command added, allowing for definition by

--- a/doc-src/IsarRef/generic.tex	Fri Aug 29 15:19:02 2003 +0200
+++ b/doc-src/IsarRef/generic.tex	Fri Aug 29 15:40:11 2003 +0200
@@ -437,7 +437,7 @@
 
 \indexisaratt{tagged}\indexisaratt{untagged}
 \indexisaratt{THEN}\indexisaratt{COMP}
-\indexisaratt{where}\indexisaratt{unfolded}\indexisaratt{folded}
+\indexisaratt{unfolded}\indexisaratt{folded}
 \indexisaratt{standard}\indexisarattof{Pure}{elim-format}
 \indexisaratt{no-vars}
 \begin{matharray}{rcl}
@@ -445,7 +445,6 @@
   untagged & : & \isaratt \\[0.5ex]
   THEN & : & \isaratt \\
   COMP & : & \isaratt \\[0.5ex]
-  where & : & \isaratt \\[0.5ex]
   unfolded & : & \isaratt \\
   folded & : & \isaratt \\[0.5ex]
   elim_format & : & \isaratt \\
@@ -460,8 +459,6 @@
   ;
   ('THEN' | 'COMP') ('[' nat ']')? thmref
   ;
-  'where' (name '=' term * 'and')
-  ;
   ('unfolded' | 'folded') thmrefs
   ;
 \end{rail}
@@ -480,11 +477,6 @@
   normally intended (cf.\ \texttt{RS} and \texttt{COMP} in
   \cite[\S5]{isabelle-ref}).
 
-\item [$where~\vec x = \vec t$] perform named instantiation of schematic
-  variables occurring in a theorem.  Unlike instantiation tactics such as
-  $rule_tac$ (see \S\ref{sec:tactic-commands}), actual schematic variables
-  have to be specified on the left-hand side (e.g.\ $\Var{x@3}$).
-
 \item [$unfolded~\vec a$ and $folded~\vec a$] expand and fold back again the
   given meta-level definitions throughout a rule.
 
@@ -513,15 +505,23 @@
 dynamic instantiation within the scope of some subgoal.
 
 \begin{warn}
-  Dynamic instantiations are read and type-checked according to a subgoal of
-  the current dynamic goal state, rather than the static proof context!  In
-  particular, locally fixed variables and term abbreviations may not be
-  included in the term specifications.  Thus schematic variables are left to
-  be solved by unification with certain parts of the subgoal involved.
+  Dynamic instantiations refer to universally quantified parameters of
+  a subgoal (the dynamic context) rather than fixed variables and term
+  abbreviations of a (static) Isar context.
 \end{warn}
 
+Tactic emulation methods, unlike their ML counterparts, admit
+simultaneous instantiation from both dynamic and static contexts.  If
+names occur in both contexts goal parameters hide locally fixed
+variables.  Likewise, schematic variables refer to term abbreviations,
+if present in the static context.  Otherwise the schematic variable is
+interpreted as a schematic variable and left to be solved by unification
+with certain parts of the subgoal.
+
 Note that the tactic emulation proof methods in Isabelle/Isar are consistently
-named $foo_tac$.
+named $foo_tac$.  Note also that variable names occurring on left hand sides
+of instantiations must be preceded by a question mark if they contain dots.
+This is consistent with the attribute $where$ (see \S\ref{sec:pure-meth-att}).
 
 \indexisarmeth{rule-tac}\indexisarmeth{erule-tac}
 \indexisarmeth{drule-tac}\indexisarmeth{frule-tac}

--- a/doc-src/IsarRef/pure.tex	Fri Aug 29 15:19:02 2003 +0200
+++ b/doc-src/IsarRef/pure.tex	Fri Aug 29 15:40:11 2003 +0200
@@ -963,7 +963,7 @@
 \indexisarmeth{this}\indexisarmeth{rule}\indexisarmeth{rules}
 \indexisarattof{Pure}{intro}\indexisarattof{Pure}{elim}
 \indexisarattof{Pure}{dest}\indexisarattof{Pure}{rule}
-\indexisaratt{OF}\indexisaratt{of}
+\indexisaratt{OF}\indexisaratt{of}\indexisaratt{where}
 \begin{matharray}{rcl}
   - & : & \isarmeth \\
   assumption & : & \isarmeth \\
@@ -976,6 +976,7 @@
   rule & : & \isaratt \\[0.5ex]
   OF & : & \isaratt \\
   of & : & \isaratt \\
+  where & : & \isaratt \\
 \end{matharray}
 
 \begin{rail}
@@ -993,6 +994,8 @@
   ;
   'of' insts ('concl' ':' insts)?
   ;
+  'where' (name '=' term * 'and')
+  ;
 \end{rail}
 
 \begin{descr}
@@ -1058,6 +1061,11 @@
   following a ``$concl\colon$'' specification refer to positions of the
   conclusion of a rule.
   
+\item [$where~\vec x = \vec t$] performs named instantiation of schematic
+  variables occurring in a theorem.  Schematic variables
+  have to be specified on the left-hand side (e.g.\ $?x1\!.\!3$).  The
+  question mark may be omitted if the variable name does not contain a dot.
+
 \end{descr}
 
 

--- a/doc-src/IsarRef/refcard.tex	Fri Aug 29 15:19:02 2003 +0200
+++ b/doc-src/IsarRef/refcard.tex	Fri Aug 29 15:40:11 2003 +0200
@@ -118,8 +118,9 @@
 
 \begin{tabular}{ll}
   \multicolumn{2}{l}{\textbf{Operations}} \\[0.5ex]
-  $OF~\vec a$ & rule applied to facts (skipping ``$_$'') \\
-  $of~\vec t$ & rule applied to terms (skipping ``$_$'') \\
+  $OF~\vec a$ & rule resolved with facts (skipping ``$_$'') \\
+  $of~\vec t$ & rule instantiated with terms (skipping ``$_$'') \\
+  $where~\vec x = \vec t$ & rule instantiated with terms, by variable name \\
   $symmetric$ & resolution with symmetry rule \\
   $THEN~b$ & resolution with another rule \\
   $rule_format$ & result put into standard rule format \\