added section on type synonyms
Thu, 24 Mar 1994 18:00:11 +0100
changeset 303 0746399cfd44
parent 302 7e2cffe28eb5
child 304 5edc4f5e5ebd
added section on type synonyms
--- a/doc-src/Intro/advanced.tex	Thu Mar 24 17:54:32 1994 +0100
+++ b/doc-src/Intro/advanced.tex	Thu Mar 24 18:00:11 1994 +0100
@@ -352,6 +352,8 @@
 rules on abstract syntax trees, for defining notations and abbreviations.
 The {\ML} section contains code to perform arbitrary syntactic
 transformations.  The main declaration forms are discussed below.
+The full syntax can be found in \iflabelundefined{app:TheorySyntax}{the
+  appendix of the {\it Reference Manual}}{Appendix~\ref{app:TheorySyntax}}.
 All the declaration parts can be omitted.  In the simplest case, $T$ is
 just the union of $S@1$,~\ldots,~$S@n$.  New theories always extend one
@@ -432,7 +434,7 @@
 \subsection{Declaring type constructors}
 Types are composed of type variables and {\bf type constructors}.  Each
 type constructor takes a fixed number of arguments.  They are declared
@@ -516,6 +518,34 @@
 translator passes them verbatim to the {\ML} output file.
+\subsection{Type synonyms}
+Isabelle supports {\bf type synonyms} ({\bf abbreviations}) which are similar
+to those found in ML. Such synonyms are defined in the type declaration part
+and are fairly self explanatory:
+types gate = "[o,o] => o"
+      'a pred = "'a => o"
+      ('a,'b)nuf = "'b => 'a"
+Type declarations and synonyms can be mixed arbitrarily:
+types nat
+      'a stream = "nat => 'a"
+      signal = "nat stream"
+      'a list
+A synonym is merely an abbreviation for some existing type expression. Hence
+synonyms may not be recursive! Internally all synonyms are fully expanded. As
+a consequence Isabelle output never contains synonyms. Their main purpose is
+to improve the readability of theories. Synonyms can be used just like any
+other type:
+consts and,or :: "gate"
+       negate :: "signal => signal"
 \subsection{Infixes and Mixfixes}
 \indexbold{infix operators}\index{examples!of theories}
 The constant declaration part of the theory