# HG changeset patch
# User nipkow
# Date 1375286892 -7200
# Node ID ba5135f45f753f3174399ad156a25eb33a18e4e9
# Parent  963297a242065bc44b4224df4206873bbfebca7f
added Getting Started text

diff -r 963297a24206 -r ba5135f45f75 src/Doc/ProgProve/document/intro-isabelle.tex
--- 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}
+
+If you have not done so already, download and install 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
 donwload and read the book
 \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