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

author | nipkow |

Fri, 03 Oct 2014 11:48:27 +0200 | |

changeset 58521 | b70e93c05efe |

parent 58520 | a4d1f8041af0 |

child 58522 | ad010811f450 |

tuned

--- a/src/Doc/Prog_Prove/Basics.thy Thu Oct 02 17:51:04 2014 +0200 +++ b/src/Doc/Prog_Prove/Basics.thy Fri Oct 03 11:48:27 2014 +0200 @@ -27,7 +27,7 @@ \item[function types,] denoted by @{text"\<Rightarrow>"}. \item[type variables,] - denoted by @{typ 'a}, @{typ 'b}, etc., just like in ML\@. + denoted by @{typ 'a}, @{typ 'b}, etc., like in ML\@. \end{description} Note that @{typ"'a \<Rightarrow> 'b list"} means @{typ[source]"'a \<Rightarrow> ('b list)"}, not @{typ"('a \<Rightarrow> 'b) list"}: postfix type constructors have precedence

--- a/src/Doc/Prog_Prove/Bool_nat_list.thy Thu Oct 02 17:51:04 2014 +0200 +++ b/src/Doc/Prog_Prove/Bool_nat_list.thy Fri Oct 03 11:48:27 2014 +0200 @@ -94,7 +94,7 @@ \begin{warn} Numerals (@{text 0}, @{text 1}, @{text 2}, \dots) and most of the standard arithmetic operations (@{text "+"}, @{text "-"}, @{text "*"}, @{text"\<le>"}, - @{text"<"} etc) are overloaded: they are available + @{text"<"}, etc.) are overloaded: they are available not just for natural numbers but for other types as well. For example, given the goal @{text"x + 0 = x"}, there is nothing to indicate that you are talking about natural numbers. Hence Isabelle can only infer @@ -150,7 +150,7 @@ \subsection{Type \indexed{@{text list}}{list}} -Although lists are already predefined, we define our own copy just for +Although lists are already predefined, we define our own copy for demonstration purposes: *} (*<*) @@ -211,7 +211,7 @@ \begin{figure}[htbp] \begin{alltt} \input{MyList.thy}\end{alltt} -\caption{A Theory of Lists} +\caption{A theory of lists} \label{fig:MyList} \index{comment} \end{figure}

--- a/src/Doc/Prog_Prove/Isar.thy Thu Oct 02 17:51:04 2014 +0200 +++ b/src/Doc/Prog_Prove/Isar.thy Fri Oct 03 11:48:27 2014 +0200 @@ -73,7 +73,7 @@ Propositions are optionally named formulas. These names can be referred to in later \isacom{from} clauses. In the simplest case, a fact is such a name. But facts can also be composed with @{text OF} and @{text of} as shown in -\S\ref{sec:forward-proof}---hence the \dots\ in the above grammar. Note +\autoref{sec:forward-proof}---hence the \dots\ in the above grammar. Note that assumptions, intermediate \isacom{have} statements and global lemmas all have the same status and are thus collectively referred to as \conceptidx{facts}{fact}. @@ -217,7 +217,7 @@ Stating a lemma with \isacom{assumes}-\isacom{shows} implicitly introduces the name \indexed{@{text assms}}{assms} that stands for the list of all assumptions. You can refer -to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"}, etc.\ +to individual assumptions by @{text"assms(1)"}, @{text"assms(2)"}, etc., thus obviating the need to name them individually. \section{Proof Patterns}

--- a/src/Doc/Prog_Prove/Types_and_funs.thy Thu Oct 02 17:51:04 2014 +0200 +++ b/src/Doc/Prog_Prove/Types_and_funs.thy Fri Oct 03 11:48:27 2014 +0200 @@ -8,11 +8,11 @@ \section{Type and Function Definitions} Type synonyms are abbreviations for existing types, for example -*} +\index{string@@{text string}}*} type_synonym string = "char list" -text{*\index{string@@{text string}} +text{* Type synonyms are expanded after parsing and are not present in internal representation and output. They are mere conveniences for the reader. \subsection{Datatypes} @@ -118,7 +118,7 @@ "sq' n \<equiv> n * n" text{* The key difference is that @{const sq'} is only syntactic sugar: -after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}}, and +after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}}; before printing, every occurrence of @{term"u*u"} is replaced by \mbox{@{term"sq' u"}}. Internally, @{const sq'} does not exist. This is the @@ -411,7 +411,7 @@ Only equations that really simplify, like @{prop"rev (rev xs) = xs"} and @{prop"xs @ [] = xs"}, should be declared as simplification rules. Equations that may be counterproductive as simplification rules -should only be used in specific proof steps (see \S\ref{sec:simp} below). +should only be used in specific proof steps (see \autoref{sec:simp} below). Distributivity laws, for example, alter the structure of terms and can produce an exponential blow-up.