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