# HG changeset patch
# User wenzelm
# Date 981148651 -3600
# Node ID 99c4bed16b9b7b8e5be7ee181f871f68bb723233
# Parent  1b709f59e33a20598524469414aab0caedff462d
isatool convert;

diff -r 1b709f59e33a -r 99c4bed16b9b doc-src/System/misc.tex
--- a/doc-src/System/misc.tex	Fri Feb 02 11:42:36 2001 +0100
+++ b/doc-src/System/misc.tex	Fri Feb 02 22:17:31 2001 +0100
@@ -3,10 +3,31 @@
 
 \chapter{Miscellaneous tools} \label{ch:tools}
 
-Subsequently we describe various Isabelle related utilities --- in
+Subsequently we describe various Isabelle related utilities, given in
 alphabetical order.
 
 
+\section{Converting legacy ML scripts --- \texttt{isatool convert}}
+
+The \tooldx{convert} utility assists in converting legacy ML proof scripts
+into the new-style format of Isabelle/Isar:
+\begin{ttbox}
+Usage: convert [FILES|DIRS...]
+
+  Recursively find .ML files, converting legacy tactic scripts to
+  Isabelle/Isar tactic emulation.
+  Note: conversion is only approximated, based on some heuristics.
+
+  Renames old versions of FILES by appending "~0~".
+  Creates new versions of FILES by appending ".thy".
+\end{ttbox}
+The resulting theory text uses the tactic emulation facilities of
+Isabelle/Isar (see also \cite{isabelle-ref}, especially the ``Conversion
+guide'' in the appendix).  Usually there is some manual tuning required to get
+an automatically converted script work again --- the success rate may be
+around 99\% for common ML scripts.
+
+
 \section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc}
 
 The \tooldx{doc} utility displays online documentation: