equal
deleted
inserted
replaced
1 |
1 |
2 % $Id$ |
2 % $Id$ |
3 |
3 |
4 \chapter{Miscellaneous tools} \label{ch:tools} |
4 \chapter{Miscellaneous tools} \label{ch:tools} |
5 |
5 |
6 Subsequently we describe various Isabelle related utilities --- in |
6 Subsequently we describe various Isabelle related utilities, given in |
7 alphabetical order. |
7 alphabetical order. |
|
8 |
|
9 |
|
10 \section{Converting legacy ML scripts --- \texttt{isatool convert}} |
|
11 |
|
12 The \tooldx{convert} utility assists in converting legacy ML proof scripts |
|
13 into the new-style format of Isabelle/Isar: |
|
14 \begin{ttbox} |
|
15 Usage: convert [FILES|DIRS...] |
|
16 |
|
17 Recursively find .ML files, converting legacy tactic scripts to |
|
18 Isabelle/Isar tactic emulation. |
|
19 Note: conversion is only approximated, based on some heuristics. |
|
20 |
|
21 Renames old versions of FILES by appending "~0~". |
|
22 Creates new versions of FILES by appending ".thy". |
|
23 \end{ttbox} |
|
24 The resulting theory text uses the tactic emulation facilities of |
|
25 Isabelle/Isar (see also \cite{isabelle-ref}, especially the ``Conversion |
|
26 guide'' in the appendix). Usually there is some manual tuning required to get |
|
27 an automatically converted script work again --- the success rate may be |
|
28 around 99\% for common ML scripts. |
8 |
29 |
9 |
30 |
10 \section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc} |
31 \section{Viewing documentation --- \texttt{isatool doc}} \label{sec:tool-doc} |
11 |
32 |
12 The \tooldx{doc} utility displays online documentation: |
33 The \tooldx{doc} utility displays online documentation: |