--- a/src/Doc/Prog_Prove/Basics.thy Tue Feb 09 09:51:55 2016 +0100
+++ b/src/Doc/Prog_Prove/Basics.thy Tue Feb 09 11:05:53 2016 +0100
@@ -140,13 +140,15 @@
message, it refers to the HOL syntax as the \concept{inner syntax} and the
enclosing theory language as the \concept{outer syntax}.
+\ifsem\else
\subsection{Proof State}
\begin{warn}
-By default Isabelle/jEdit does not show the proof state
-in the output window. You should enable this by ticking the
-``Proof state'' box.
+By default Isabelle/jEdit does not show the proof state but this tutorial
+refers to it frequently. You should tick the ``Proof state'' box
+to see the proof state in the output window.
\end{warn}
+\fi
*}
(*<*)
end
--- a/src/Doc/Prog_Prove/Bool_nat_list.thy Tue Feb 09 09:51:55 2016 +0100
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Tue Feb 09 11:05:53 2016 +0100
@@ -58,7 +58,8 @@
need to be established by induction in most cases.
Command \isacom{apply}@{text"(induction m)"} instructs Isabelle to
start a proof by induction on @{text m}. In response, it will show the
-following proof state:
+following proof state\ifsem\footnote{See page \pageref{proof-state} for how to
+display the proof state}\fi:
@{subgoals[display,indent=0]}
The numbered lines are known as \emph{subgoals}.
The first subgoal is the base case, the second one the induction step.
--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Tue Feb 09 09:51:55 2016 +0100
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Tue Feb 09 11:05:53 2016 +0100
@@ -59,7 +59,7 @@
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
+a typical example snapshot of a session. At this point we merely explain
the layout of the window, not its contents.
\begin{center}
@@ -72,7 +72,13 @@
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.
+\begin{warn}
+By default Isabelle/jEdit does not show the proof state but this book
+refers to it frequently. You should tick the ``Proof state'' box
+to see the proof state in the output window.
+\end{warn}
+
+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