# HG changeset patch
# User wenzelm
# Date 963522500 -7200
# Node ID 4adf25becaa4b311ef633612e38305848e2b2e3e
# Parent  5613e184b8b347fc1c13f69b7f38dd1aa31f4ad6
defs: (overloaded) option;

diff -r 5613e184b8b3 -r 4adf25becaa4 doc-src/IsarRef/pure.tex
--- a/doc-src/IsarRef/pure.tex	Thu Jul 13 23:07:56 2000 +0200
+++ b/doc-src/IsarRef/pure.tex	Thu Jul 13 23:08:20 2000 +0200
@@ -230,7 +230,7 @@
 \begin{rail}
   'consts' (constdecl +)
   ;
-  'defs' (axmdecl prop comment? +)
+  'defs' ('(overloaded)')? (axmdecl prop comment? +)
   ;
   'constdefs' (constdecl prop comment? +)
   ;
@@ -243,9 +243,16 @@
 \item [$\CONSTS~c::\sigma$] declares constant $c$ to have any instance of type
   scheme $\sigma$.  The optional mixfix annotations may attach concrete syntax
   to the constants declared.
+
 \item [$\DEFS~name: eqn$] introduces $eqn$ as a definitional axiom for some
   existing constant.  See \cite[\S6]{isabelle-ref} for more details on the
   form of equations admitted as constant definitions.
+  
+  The $overloaded$ option declares definitions to be potentially overloaded.
+  Unless this option is given, a warning message would be issued for any
+  definitional equation with a more special type than that of the
+  corresponding constant declaration.
+
 \item [$\isarkeyword{constdefs}~c::\sigma~eqn$] combines declarations and
   definitions of constants, using the canonical name $c_def$ for the
   definitional axiom.