--- 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.
--- 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.