# HG changeset patch
# User wenzelm
# Date 967923964 -7200
# Node ID 21b36757a9a5739c8f5586ed10474c091a418ff7
# Parent  49e55730eb7afedce924104129ab49f3439922c4
some stuff;

diff -r 49e55730eb7a -r 21b36757a9a5 doc-src/IsarRef/conversion.tex
--- a/doc-src/IsarRef/conversion.tex	Sat Sep 02 21:45:41 2000 +0200
+++ b/doc-src/IsarRef/conversion.tex	Sat Sep 02 21:46:04 2000 +0200
@@ -8,6 +8,23 @@
 
 \section{Porting proof scripts}
 
+FIXME
+
+\subsection{Basic tactics}
+
+\begin{matharray}{llll}
+  \texttt{rtac}~a~1 & & rule~a \\
+  \texttt{resolve_tac}~[a@1, \dots, a@n]~1 & & rule~a@1~\dots~a@n \\
+  \texttt{res_inst_tac}~[(x@1, t@1), \dots, (x@n, t@n)]~a~1 & &
+  rule_tac~x@1 = t@1~\dots~x@n = t@n~\textrm{in}~a \\
+  
+%  \texttt{} & & \\
+  \texttt{stac}~a~1 & & subst~a \\
+  \texttt{strip_tac}~1 & & intro~strip & \Text{(HOL)} \\
+  \texttt{split_all_tac} & \ll & clarify & \Text{(HOL)} \\
+\end{matharray}
+
+
 \section{Performing actual proof}
 
 FIXME