merged
authornipkow
Mon Jan 09 19:34:16 2017 +0100 (2017-01-09)
changeset 648539178214b3588
parent 64850 fc9265882329
parent 64852 f3504bc69ea3
child 64854 f5aa712e6250
merged
     1.1 --- a/src/Doc/Prog_Prove/Isar.thy	Mon Jan 09 19:13:49 2017 +0100
     1.2 +++ b/src/Doc/Prog_Prove/Isar.thy	Mon Jan 09 19:34:16 2017 +0100
     1.3 @@ -109,7 +109,7 @@
     1.4  {\mbox{@{thm (concl) notI}}}
     1.5  \]
     1.6  In order to prove @{prop"~ P"}, assume @{text P} and show @{text False}.
     1.7 -Thus we may assume @{prop"surj f"}. The proof shows that names of propositions
     1.8 +Thus we may assume \mbox{\noquotes{@{prop [source] "surj f"}}}. The proof shows that names of propositions
     1.9  may be (single!) digits --- meaningful names are hard to invent and are often
    1.10  not necessary. Both \isacom{have} steps are obvious. The second one introduces
    1.11  the diagonal set @{term"{x. x \<notin> f x}"}, the key idea in the proof.
    1.12 @@ -178,7 +178,7 @@
    1.13  \subsection{Structured Lemma Statements: \indexed{\isacom{fixes}}{fixes}, \indexed{\isacom{assumes}}{assumes}, \indexed{\isacom{shows}}{shows}}
    1.14  \index{lemma@\isacom{lemma}}
    1.15  Lemmas can also be stated in a more structured fashion. To demonstrate this
    1.16 -feature with Cantor's theorem, we rephrase @{prop"\<not> surj f"}
    1.17 +feature with Cantor's theorem, we rephrase \noquotes{@{prop[source]"\<not> surj f"}}
    1.18  a little:
    1.19  *}
    1.20  
    1.21 @@ -193,8 +193,8 @@
    1.22  the \isacom{assumes} part that allows you to name each assumption; multiple
    1.23  assumptions can be separated by \isacom{and}. The
    1.24  \isacom{shows} part gives the goal. The actual theorem that will come out of
    1.25 -the proof is @{prop"surj f \<Longrightarrow> False"}, but during the proof the assumption
    1.26 -@{prop"surj f"} is available under the name @{text s} like any other fact.
    1.27 +the proof is \noquotes{@{prop[source]"surj f \<Longrightarrow> False"}}, but during the proof the assumption
    1.28 +\noquotes{@{prop[source]"surj f"}} is available under the name @{text s} like any other fact.
    1.29  *}
    1.30  
    1.31  proof -
    1.32 @@ -210,8 +210,8 @@
    1.33  Isabelle to try some suitable introduction rule on the goal @{const False} --- but
    1.34  there is no such rule and \isacom{proof} would fail.
    1.35  \end{warn}
    1.36 -In the \isacom{have} step the assumption @{prop"surj f"} is now
    1.37 -referenced by its name @{text s}. The duplication of @{prop"surj f"} in the
    1.38 +In the \isacom{have} step the assumption \noquotes{@{prop[source]"surj f"}} is now
    1.39 +referenced by its name @{text s}. The duplication of \noquotes{@{prop[source]"surj f"}} in the
    1.40  above proofs (once in the statement of the lemma, once in its proof) has been
    1.41  eliminated.
    1.42  
     2.1 --- a/src/Doc/Prog_Prove/document/intro-isabelle.tex	Mon Jan 09 19:13:49 2017 +0100
     2.2 +++ b/src/Doc/Prog_Prove/document/intro-isabelle.tex	Mon Jan 09 19:34:16 2017 +0100
     2.3 @@ -55,7 +55,7 @@
     2.4  \subsection*{Getting Started with Isabelle}
     2.5  
     2.6  If you have not done so already, download and install Isabelle
     2.7 -(this book is compatible with Isabelle2016)
     2.8 +(this book is compatible with Isabelle2016-1)
     2.9  from \url{http://isabelle.in.tum.de}. You can start it by clicking
    2.10  on the application icon. This will launch Isabelle's
    2.11  user interface based on the text editor \concept{jEdit}. Below you see
    2.12 @@ -74,9 +74,8 @@
    2.13  
    2.14  \begin{warn}\label{proof-state}
    2.15  Part I frequently refers to the proof state.
    2.16 -You can see the proof state combined with other system output if you
    2.17 -press the ``Output'' button to open the output area and tick the 
    2.18 -``Proof state'' box to see the proof state in the output area.
    2.19 +You can see the proof state if you press the ``State'' button.
    2.20 +If you want to see the proof state combined with other system output, press ``Output'' and tick the ``Proof state'' box.
    2.21  \end{warn}
    2.22  
    2.23  This should suffice to get started with the jEdit interface.
     3.1 --- a/src/HOL/IMP/Hoare_Examples.thy	Mon Jan 09 19:13:49 2017 +0100
     3.2 +++ b/src/HOL/IMP/Hoare_Examples.thy	Mon Jan 09 19:34:16 2017 +0100
     3.3 @@ -2,6 +2,8 @@
     3.4  
     3.5  theory Hoare_Examples imports Hoare begin
     3.6  
     3.7 +hide_const (open) sum
     3.8 +
     3.9  text{* Summing up the first @{text x} natural numbers in variable @{text y}. *}
    3.10  
    3.11  fun sum :: "int \<Rightarrow> int" where