| changeset 42637 | 381fdcab0f36 |
| parent 14148 | 6580d374a509 |
| child 43077 | 7d69154d824b |
--- a/doc-src/Intro/getting.tex Mon May 02 22:19:28 2011 +0200 +++ b/doc-src/Intro/getting.tex Mon May 02 22:31:46 2011 +0200 @@ -1,4 +1,3 @@ -%% $Id$ \part{Using Isabelle from the ML Top-Level}\label{chap:getting} Most Isabelle users write proof scripts using the Isar language, as described in the \emph{Tutorial}, and debug them through the Proof General user interface~\cite{proofgeneral}. Isabelle's original user interface --- based on the \ML{} top-level --- is still available, however.