summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Mon, 09 Jan 2017 19:34:16 +0100 | |

changeset 64853 | 9178214b3588 |

parent 64850 | fc9265882329 (current diff) |

parent 64852 | f3504bc69ea3 (diff) |

child 64854 | f5aa712e6250 |

merged

--- a/src/Doc/Prog_Prove/Isar.thy Mon Jan 09 19:13:49 2017 +0100 +++ b/src/Doc/Prog_Prove/Isar.thy Mon Jan 09 19:34:16 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:13:49 2017 +0100 +++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex Mon Jan 09 19:34:16 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.

--- a/src/HOL/IMP/Hoare_Examples.thy Mon Jan 09 19:13:49 2017 +0100 +++ b/src/HOL/IMP/Hoare_Examples.thy Mon Jan 09 19:34:16 2017 +0100 @@ -2,6 +2,8 @@ theory Hoare_Examples imports Hoare begin +hide_const (open) sum + text{* Summing up the first @{text x} natural numbers in variable @{text y}. *} fun sum :: "int \<Rightarrow> int" where