# HG changeset patch
# User wenzelm
# Date 954421982 -7200
# Node ID 3786d47f5570127b6df55595e457b3a9b7071a9d
# Parent  63a0e1502e411ceeb52d30be8e3c361d7d4e7162
support Hindley-Milner polymorphisms in results and bindings;

diff -r 63a0e1502e41 -r 3786d47f5570 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Thu Mar 30 15:12:20 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Thu Mar 30 15:13:02 2000 +0200
@@ -833,10 +833,21 @@
 patterns occur on the left-hand side, while the $\ISNAME$ patterns are in
 postfix position.
 
+Polymorphism of term bindings is handled in Hindley-Milner style, as in ML.
+Type variables referring to local assumptions or open goal statements are
+\emph{fixed}, while those of finished results or bound by $\LETNAME$ may occur
+in \emph{arbitrary} instances later.  Even though actual polymorphism should
+be rarely used in practice, this mechanism is essential to achieve proper
+incremental type-inference, as the user proceeds to build up the Isar proof
+text.
+
+\medskip
+
 Term abbreviations are quite different from actual local definitions as
 introduced via $\DEFNAME$ (see \S\ref{sec:proof-context}).  The latter are
 visible within the logic as actual equations, while abbreviations disappear
-during the input process just after type checking.
+during the input process just after type checking.  Also note that $\DEFNAME$
+does not support polymorphism.
 
 \begin{rail}
   'let' ((term + 'as') '=' term comment? + 'and')