author nipkow Wed, 31 Jul 2013 18:08:12 +0200 changeset 52814 ba5135f45f75 parent 52813 963297a24206 child 52815 eaad5fe7bb1b
--- a/src/Doc/ProgProve/document/intro-isabelle.tex	Wed Jul 31 16:50:41 2013 +0200
+++ b/src/Doc/ProgProve/document/intro-isabelle.tex	Wed Jul 31 18:08:12 2013 +0200
@@ -51,7 +51,29 @@
%This introduction to Isabelle has grown out of many years of teaching
%Isabelle courses.

-\ifsem\else
+\ifsem
+\subsection*{Getting Started with Isabelle}
+
+from \url{http://isabelle.in.tum.de}. You can start it by clicking
+on the application icon. This will launch Isabelle's
+user interface based on the text editor \concept{jedit}. Below you see
+a typical example snapshot of a jedit session. At this point we merely explain
+the layout of the window, not its contents.
+
+\begin{center}
+\includegraphics[width=\textwidth]{jedit.png}
+\end{center}
+The upper part of the window shows the input typed by the user, i.e.\ the
+gradually growing Isabelle text of definitions, theorems, proofs, etc.  The
+interface processes the user input automatically while it is typed, just like
+modern Java IDEs.  Isabelle's response to the user input is shown in the
+lower part of the window. You can examine the response to any input phrase
+by clicking on that phrase or by hovering over underlined text.
+
+This should suffice to get started with the jedit interface.
+Now you need to learn what to type into it.
+\else
If you want to apply what you have learned about Isabelle we recommend you
\href{http://www.in.tum.de/~nipkow/Concrete/}{Concrete
@@ -64,6 +86,9 @@
Proving in Isabelle/HOL}.
\fi

+\ifsem\else
\paragraph{Acknowledgements}
-\ifsem We \else I \fi wish to thank the following people for their comments:
-Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel.
\ No newline at end of file
+I wish to thank the following people for their comments
+on this document:
+Florian Haftmann, Ren\'{e} Thiemann and Christian Sternagel.
+\fi
\ No newline at end of file