Fri, 17 May 2013 02:57:00 +0200
changeset 52045 90cd3c53a887
parent 52044 16c4e428a1d4
child 52046 bc01725d7918
--- 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\@.
+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}.
-In the Isabelle part of the book we show all quotation marks.
-In the Semantics part we omit them for reasons of readability.
--- 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}