# HG changeset patch
# User nipkow
# Date 1455032323 -3600
# Node ID c82c7b78b509f9c22b9c7bfa9560e310093ba015
# Parent  54a7b9422d3ebe04e607977cfe31c198041c1a7c
tuned

diff -r 54a7b9422d3e -r c82c7b78b509 src/Doc/Prog_Prove/Bool_nat_list.thy
--- 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.
diff -r 54a7b9422d3e -r c82c7b78b509 src/Doc/Prog_Prove/Logic.thy
--- 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}
diff -r 54a7b9422d3e -r c82c7b78b509 src/Doc/Prog_Prove/document/intro-isabelle.tex
--- 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.