# HG changeset patch
# User nipkow
# Date 1483986842 -3600
# Node ID f3504bc69ea3dc42522638069089916c60a6ae4c
# Parent  33aab75ff4238049bd61a90513ce266b2ccf2114
fix problems because of "surj" input abbreviation; tuned

diff -r 33aab75ff423 -r f3504bc69ea3 src/Doc/Prog_Prove/Isar.thy
--- a/src/Doc/Prog_Prove/Isar.thy	Mon Jan 09 19:32:40 2017 +0100
+++ b/src/Doc/Prog_Prove/Isar.thy	Mon Jan 09 19:34:02 2017 +0100
@@ -109,7 +109,7 @@
 {\mbox{@{thm (concl) notI}}}
 \]
 In order to prove @{prop"~ P"}, assume @{text P} and show @{text False}.
-Thus we may assume @{prop"surj f"}. The proof shows that names of propositions
+Thus we may assume \mbox{\noquotes{@{prop [source] "surj f"}}}. The proof shows that names of propositions
 may be (single!) digits --- meaningful names are hard to invent and are often
 not necessary. Both \isacom{have} steps are obvious. The second one introduces
 the diagonal set @{term"{x. x \<notin> f x}"}, the key idea in the proof.
@@ -178,7 +178,7 @@
 \subsection{Structured Lemma Statements: \indexed{\isacom{fixes}}{fixes}, \indexed{\isacom{assumes}}{assumes}, \indexed{\isacom{shows}}{shows}}
 \index{lemma@\isacom{lemma}}
 Lemmas can also be stated in a more structured fashion. To demonstrate this
-feature with Cantor's theorem, we rephrase @{prop"\<not> surj f"}
+feature with Cantor's theorem, we rephrase \noquotes{@{prop[source]"\<not> surj f"}}
 a little:
 *}
 
@@ -193,8 +193,8 @@
 the \isacom{assumes} part that allows you to name each assumption; multiple
 assumptions can be separated by \isacom{and}. The
 \isacom{shows} part gives the goal. The actual theorem that will come out of
-the proof is @{prop"surj f \<Longrightarrow> False"}, but during the proof the assumption
-@{prop"surj f"} is available under the name @{text s} like any other fact.
+the proof is \noquotes{@{prop[source]"surj f \<Longrightarrow> False"}}, but during the proof the assumption
+\noquotes{@{prop[source]"surj f"}} is available under the name @{text s} like any other fact.
 *}
 
 proof -
@@ -210,8 +210,8 @@
 Isabelle to try some suitable introduction rule on the goal @{const False} --- but
 there is no such rule and \isacom{proof} would fail.
 \end{warn}
-In the \isacom{have} step the assumption @{prop"surj f"} is now
-referenced by its name @{text s}. The duplication of @{prop"surj f"} in the
+In the \isacom{have} step the assumption \noquotes{@{prop[source]"surj f"}} is now
+referenced by its name @{text s}. The duplication of \noquotes{@{prop[source]"surj f"}} in the
 above proofs (once in the statement of the lemma, once in its proof) has been
 eliminated.
 
diff -r 33aab75ff423 -r f3504bc69ea3 src/Doc/Prog_Prove/document/intro-isabelle.tex
--- a/src/Doc/Prog_Prove/document/intro-isabelle.tex	Mon Jan 09 19:32:40 2017 +0100
+++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex	Mon Jan 09 19:34:02 2017 +0100
@@ -55,7 +55,7 @@
 \subsection*{Getting Started with Isabelle}
 
 If you have not done so already, download and install Isabelle
-(this book is compatible with Isabelle2016)
+(this book is compatible with Isabelle2016-1)
 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
@@ -74,9 +74,8 @@
 
 \begin{warn}\label{proof-state}
 Part I frequently refers to the proof state.
-You can see the proof state combined with other system output if you
-press the ``Output'' button to open the output area and tick the 
-``Proof state'' box to see the proof state in the output area.
+You can see the proof state if you press the ``State'' button.
+If you want to see the proof state combined with other system output, press ``Output'' and tick the ``Proof state'' box.
 \end{warn}
 
 This should suffice to get started with the jEdit interface.