# HG changeset patch
# User nipkow
# Date 1407397684 -7200
# Node ID fcf966675478b98490766efa5b0f5ab0e94ab801
# Parent  19f54b090cdd894a4c93c82fbe1d838db97e1adc
tuned

diff -r 19f54b090cdd -r fcf966675478 src/Doc/Prog_Prove/Basics.thy
--- 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}\\
diff -r 19f54b090cdd -r fcf966675478 src/Doc/Prog_Prove/MyList.thy
--- 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
diff -r 19f54b090cdd -r fcf966675478 src/Doc/Prog_Prove/Types_and_funs.thy
--- 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}