--- a/src/Doc/Prog_Prove/Basics.thy Wed Aug 06 18:20:31 2014 +0200
+++ b/src/Doc/Prog_Prove/Basics.thy Thu Aug 07 09:48:04 2014 +0200
@@ -73,10 +73,9 @@
called \concept{type inference}. Despite type inference, it is sometimes
necessary to attach an explicit \concept{type constraint} (or \concept{type
annotation}) to a variable or term. The syntax is @{text "t :: \<tau>"} as in
-\mbox{\noquotes{@{prop[source] "m < (n::nat)"}}}. Type constraints may be
+\mbox{\noquotes{@{term[source] "m + (n::nat)"}}}. Type constraints may be
needed to
-disambiguate terms involving overloaded functions such as @{text "+"}, @{text
-"*"} and @{text"\<le>"}.
+disambiguate terms involving overloaded functions such as @{text "+"}.
Finally there are the universal quantifier @{text"\<And>"}\index{$4@\isasymAnd} and the implication
@{text"\<Longrightarrow>"}\index{$3@\isasymLongrightarrow}. They are part of the Isabelle framework, not the logic
@@ -100,7 +99,7 @@
Roughly speaking, a \concept{theory} is a named collection of types,
functions, and theorems, much like a module in a programming language.
-All the Isabelle text that you ever type needs to go into a theory.
+All Isabelle text needs to go into a theory.
The general format of a theory @{text T} is
\begin{quote}
\indexed{\isacom{theory}}{theory} @{text T}\\
--- a/src/Doc/Prog_Prove/MyList.thy Wed Aug 06 18:20:31 2014 +0200
+++ b/src/Doc/Prog_Prove/MyList.thy Thu Aug 07 09:48:04 2014 +0200
@@ -14,4 +14,6 @@
value "rev(Cons True (Cons False Nil))"
+(* a comment *)
+
end
--- a/src/Doc/Prog_Prove/Types_and_funs.thy Wed Aug 06 18:20:31 2014 +0200
+++ b/src/Doc/Prog_Prove/Types_and_funs.thy Thu Aug 07 09:48:04 2014 +0200
@@ -93,8 +93,9 @@
text{*
Note that @{text"\<tau>\<^sub>1 * \<tau>\<^sub>2"} is the type of pairs, also written @{text"\<tau>\<^sub>1 \<times> \<tau>\<^sub>2"}.
Pairs can be taken apart either by pattern matching (as above) or with the
-projection functions @{const fst} and @{const snd}: @{thm fst_conv} and @{thm snd_conv}. Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}
-abbreviates @{text"(a, (b, c))"} and @{text "\<tau>\<^sub>1 \<times> \<tau>\<^sub>2 \<times> \<tau>\<^sub>3"} abbreviates
+projection functions @{const fst} and @{const snd}: @{thm fst_conv[of x y]} and @{thm snd_conv[of x y]}.
+Tuples are simulated by pairs nested to the right: @{term"(a,b,c)"}
+is short for @{text"(a, (b, c))"} and @{text "\<tau>\<^sub>1 \<times> \<tau>\<^sub>2 \<times> \<tau>\<^sub>3"} is short for
@{text "\<tau>\<^sub>1 \<times> (\<tau>\<^sub>2 \<times> \<tau>\<^sub>3)"}.
\subsection{Definitions}