# HG changeset patch
# User wenzelm
# Date 1213478400 -7200
# Node ID 2a8d03e0bbb97b6bc45927f5980a8ff664e5a3fc
# Parent  388fd72e9f265e619e53a73b19469554d60a1ca8
updated geenrated file;

diff -r 388fd72e9f26 -r 2a8d03e0bbb9 doc-src/IsarRef/Thy/document/Generic.tex
--- a/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 14 23:19:57 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Generic.tex	Sat Jun 14 23:20:00 2008 +0200
@@ -324,25 +324,26 @@
 \begin{descr}
 
   \item [\hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} etc.] do resolution of rules with explicit
-  instantiation.  This works the same way as the ML tactics \verb|res_inst_tac| etc. (see \cite[\S3]{isabelle-ref}).
+  instantiation.  This works the same way as the ML tactics \verb|Tactic.res_inst_tac| etc. (see \cite[\S3]{isabelle-ref})
 
   Multiple rules may be only given if there is no instantiation; then
   \hyperlink{method.rule-tac}{\mbox{\isa{rule{\isacharunderscore}tac}}} is the same as \verb|resolve_tac| in ML (see
   \cite[\S3]{isabelle-ref}).
 
   \item [\hyperlink{method.cut-tac}{\mbox{\isa{cut{\isacharunderscore}tac}}}] inserts facts into the proof state as
-  assumption of a subgoal, see also \verb|cut_facts_tac| in
+  assumption of a subgoal, see also \verb|Tactic.cut_facts_tac| in
   \cite[\S3]{isabelle-ref}.  Note that the scope of schematic
   variables is spread over the main goal statement.  Instantiations
-  may be given as well, see also ML tactic \verb|cut_inst_tac| in
-  \cite[\S3]{isabelle-ref}.
+  may be given as well, see also ML tactic \verb|Tactic.cut_inst_tac|
+  in \cite[\S3]{isabelle-ref}.
 
   \item [\hyperlink{method.thin-tac}{\mbox{\isa{thin{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] deletes the specified
   assumption from a subgoal; note that \isa{{\isasymphi}} may contain schematic
-  variables.  See also \verb|thin_tac| in \cite[\S3]{isabelle-ref}.
+  variables.  See also \verb|Tactic.thin_tac| in
+  \cite[\S3]{isabelle-ref}.
 
   \item [\hyperlink{method.subgoal-tac}{\mbox{\isa{subgoal{\isacharunderscore}tac}}}~\isa{{\isasymphi}}] adds \isa{{\isasymphi}} as an
-  assumption to a subgoal.  See also \verb|subgoal_tac| and \verb|subgoals_tac| in \cite[\S3]{isabelle-ref}.
+  assumption to a subgoal.  See also \verb|Tactic.subgoal_tac| and \verb|Tactic.subgoals_tac| in \cite[\S3]{isabelle-ref}.
 
   \item [\hyperlink{method.rename-tac}{\mbox{\isa{rename{\isacharunderscore}tac}}}~\isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}\ {\isasymdots}\ x\isactrlsub n{\isachardoublequote}}] renames
   parameters of a goal according to the list \isa{{\isachardoublequote}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharcomma}\ x\isactrlsub n{\isachardoublequote}}, which refers to the \emph{suffix} of variables.
diff -r 388fd72e9f26 -r 2a8d03e0bbb9 doc-src/IsarRef/Thy/document/ML_Tactic.tex
--- a/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Sat Jun 14 23:19:57 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/ML_Tactic.tex	Sat Jun 14 23:20:00 2008 +0200
@@ -60,7 +60,7 @@
   \verb|forward_tac|).
 
   \item Optional explicit instantiation (e.g.\ \verb|resolve_tac| vs.\
-  \verb|res_inst_tac|).
+  \verb|RuleInsts.res_inst_tac|).
 
   \item Abbreviations for singleton arguments (e.g.\ \verb|resolve_tac|
   vs.\ \verb|rtac|).
@@ -85,11 +85,11 @@
   \begin{tabular}{lll}
     \verb|rtac|~\isa{{\isachardoublequote}a\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a{\isachardoublequote}} \\
     \verb|resolve_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ {\isadigit{1}}{\isachardoublequote}} & & \isa{{\isachardoublequote}rule\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}{\isachardoublequote}} \\
-    \verb|res_inst_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ {\isadigit{1}}{\isachardoublequote}} & &
+    \verb|RuleInsts.res_inst_tac|~\isa{{\isachardoublequote}ctxt\ {\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ {\isadigit{1}}{\isachardoublequote}} & &
     \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\[0.5ex]
     \verb|rtac|~\isa{{\isachardoublequote}a\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a{\isachardoublequote}} \\
     \verb|resolve_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}a\isactrlsub {\isadigit{1}}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ i{\isachardoublequote}} & & \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ a\isactrlsub {\isadigit{1}}\ {\isasymdots}{\isachardoublequote}} \\
-    \verb|res_inst_tac|~\isa{{\isachardoublequote}{\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ i{\isachardoublequote}} & &
+    \verb|RuleInsts.res_inst_tac|~\isa{{\isachardoublequote}ctxt\ {\isacharbrackleft}{\isacharparenleft}x\isactrlsub {\isadigit{1}}{\isacharcomma}\ t\isactrlsub {\isadigit{1}}{\isacharparenright}{\isacharcomma}\ {\isasymdots}{\isacharbrackright}\ a\ i{\isachardoublequote}} & &
     \isa{{\isachardoublequote}rule{\isacharunderscore}tac\ {\isacharbrackleft}i{\isacharbrackright}\ x\isactrlsub {\isadigit{1}}\ {\isacharequal}\ t\isactrlsub {\isadigit{1}}\ {\isasymAND}\ {\isasymdots}\ {\isasymIN}\ a{\isachardoublequote}} \\
   \end{tabular}
   \medskip
diff -r 388fd72e9f26 -r 2a8d03e0bbb9 doc-src/IsarRef/Thy/document/Spec.tex
--- a/doc-src/IsarRef/Thy/document/Spec.tex	Sat Jun 14 23:19:57 2008 +0200
+++ b/doc-src/IsarRef/Thy/document/Spec.tex	Sat Jun 14 23:20:00 2008 +0200
@@ -1262,16 +1262,12 @@
     \indexdef{}{command}{print\_translation}\hypertarget{command.print-translation}{\hyperlink{command.print-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
     \indexdef{}{command}{typed\_print\_translation}\hypertarget{command.typed-print-translation}{\hyperlink{command.typed-print-translation}{\mbox{\isa{\isacommand{typed{\isacharunderscore}print{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
     \indexdef{}{command}{print\_ast\_translation}\hypertarget{command.print-ast-translation}{\hyperlink{command.print-ast-translation}{\mbox{\isa{\isacommand{print{\isacharunderscore}ast{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
-    \indexdef{}{command}{token\_translation}\hypertarget{command.token-translation}{\hyperlink{command.token-translation}{\mbox{\isa{\isacommand{token{\isacharunderscore}translation}}}}} & : & \isartrans{theory}{theory} \\
   \end{matharray}
 
   \begin{rail}
   ( 'parse\_ast\_translation' | 'parse\_translation' | 'print\_translation' |
     'typed\_print\_translation' | 'print\_ast\_translation' ) ('(advanced)')? text
   ;
-
-  'token\_translation' text
-  ;
   \end{rail}
 
   Syntax translation functions written in ML admit almost arbitrary
@@ -1287,8 +1283,6 @@
 val typed_print_translation :
   (string * (bool -> typ -> term list -> term)) list
 val print_ast_translation   : (string * (ast list -> ast)) list
-val token_translation       :
-  (string * string * (string -> string * real)) list
 \end{ttbox}
 
   If the \isa{{\isachardoublequote}{\isacharparenleft}advanced{\isacharparenright}{\isachardoublequote}} option is given, the corresponding