--- 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
--- 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}