# 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