# HG changeset patch
# User nipkow
# Date 1455012353 -3600
# Node ID 54a7b9422d3ebe04e607977cfe31c198041c1a7c
# Parent  0628123e9d4e5fe26529b51936563b00e51fbe25
synchronized with book

diff -r 0628123e9d4e -r 54a7b9422d3e src/Doc/Prog_Prove/Basics.thy
--- 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
diff -r 0628123e9d4e -r 54a7b9422d3e src/Doc/Prog_Prove/Bool_nat_list.thy
--- 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.
diff -r 0628123e9d4e -r 54a7b9422d3e src/Doc/Prog_Prove/document/intro-isabelle.tex
--- 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