| changeset 12621 | 48cafea0684b |
| parent 12618 | 43a97a2155d0 |
| child 13013 | 4db07fc3d96f |
--- a/doc-src/IsarRef/conversion.tex Thu Jan 03 17:01:59 2002 +0100 +++ b/doc-src/IsarRef/conversion.tex Thu Jan 03 17:48:02 2002 +0100 @@ -508,7 +508,7 @@ declare the theorem otherwise later (e.g.\ as $[simp~del]$). -\section{Converting to actual Isar proof texts} +\section{Writing actual Isar proof texts} Porting legacy ML proof scripts into Isar tactic emulation scripts (see \S\ref{sec:port-scripts}) is mainly a technical issue, since the basic