# HG changeset patch
# User nipkow
# Date 1368752220 -7200
# Node ID 90cd3c53a887ceed96ec00c3c97cd2e0d8bfb89e
# Parent  16c4e428a1d422cbad1af328c96433af587dcb3e
tuned

diff -r 16c4e428a1d4 -r 90cd3c53a887 src/Doc/ProgProve/Basics.thy
--- a/src/Doc/ProgProve/Basics.thy	Thu May 16 22:02:01 2013 +0200
+++ b/src/Doc/ProgProve/Basics.thy	Fri May 17 02:57:00 2013 +0200
@@ -29,6 +29,9 @@
 \item[type variables,]
   denoted by @{typ 'a}, @{typ 'b} etc., just 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
+over @{text"\<Rightarrow>"}.
 
 \concept{Terms} are formed as in functional programming by
 applying functions to arguments. If @{text f} is a function of type
@@ -136,13 +139,6 @@
 single identifier can be dropped.  When Isabelle prints a syntax error
 message, it refers to the HOL syntax as the \concept{inner syntax} and the
 enclosing theory language as the \concept{outer syntax}.
-\sem
-\begin{warn}
-In the Isabelle part of the book we show all quotation marks.
-In the Semantics part we omit them for reasons of readability.
-\end{warn}
-\endsem
-%
 *}
 (*<*)
 end
diff -r 16c4e428a1d4 -r 90cd3c53a887 src/Doc/ProgProve/Types_and_funs.thy
--- a/src/Doc/ProgProve/Types_and_funs.thy	Thu May 16 22:02:01 2013 +0200
+++ b/src/Doc/ProgProve/Types_and_funs.thy	Fri May 17 02:57:00 2013 +0200
@@ -114,18 +114,21 @@
 *}
 
 abbreviation sq' :: "nat \<Rightarrow> nat" where
-"sq' n == n * n"
+"sq' n \<equiv> n * n"
 
 text{* The key difference is that @{const sq'} is only syntactic sugar:
-@{term"sq' t"} is replaced by \mbox{@{term"t*t"}} after parsing, and every
-occurrence of a term @{term"u*u"} is replaced by \mbox{@{term"sq' u"}} before
-printing.  Internally, @{const sq'} does not exist.  This is also the
+after parsing, @{term"sq' t"} is replaced by \mbox{@{term"t*t"}}, and
+before printing, every occurrence of @{term"u*u"} is replaced by
+\mbox{@{term"sq' u"}}.  Internally, @{const sq'} does not exist.
+This is the
 advantage of abbreviations over definitions: definitions need to be expanded
-explicitly (see \autoref{sec:rewr-defs}) whereas abbreviations are already
+explicitly (\autoref{sec:rewr-defs}) whereas abbreviations are already
 expanded upon parsing. However, abbreviations should be introduced sparingly:
 if abused, they can lead to a confusing discrepancy between the internal and
 external view of a term.
 
+The ASCII representation of @{text"\<equiv>"} is \texttt{==} or \xsymbol{equiv}.
+
 \subsection{Recursive functions}
 \label{sec:recursive-funs}