--- a/src/Doc/Prog_Prove/Bool_nat_list.thy Tue Feb 09 11:05:53 2016 +0100
+++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Tue Feb 09 16:38:43 2016 +0100
@@ -59,7 +59,7 @@
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\ifsem\footnote{See page \pageref{proof-state} for how to
-display the proof state}\fi:
+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/Logic.thy Tue Feb 09 11:05:53 2016 +0100
+++ b/src/Doc/Prog_Prove/Logic.thy Tue Feb 09 16:38:43 2016 +0100
@@ -134,7 +134,7 @@
\begin{tabular}{l@ {\quad}l}
@{const_typ set}\index{set@@{const set}} & converts a list to the set of its elements\\
@{const_typ finite}\index{finite@@{const finite}} & is true iff its argument is finite\\
-@{const_typ card}\index{card@@{const card}} & is the cardinality of a finite set\\
+\noquotes{@{term[source] "card :: 'a set \<Rightarrow> nat"}}\index{card@@{const card}} & is the cardinality of a finite set\\
& and is @{text 0} for all infinite sets\\
@{thm image_def}\index{$IMP042@@{term"f ` A"}} & is the image of a function over a set
\end{tabular}
--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex Tue Feb 09 11:05:53 2016 +0100
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Tue Feb 09 16:38:43 2016 +0100
@@ -72,7 +72,7 @@
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.
-\begin{warn}
+\begin{warn}\label{proof-state}
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.