--- 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