--- a/doc-src/IsarRef/generic.tex Wed Jun 01 10:52:17 2005 +0200
+++ b/doc-src/IsarRef/generic.tex Wed Jun 01 12:30:49 2005 +0200
@@ -122,10 +122,12 @@
contextexpr: nameref | '(' contextexpr ')' |
(contextexpr (name mixfix? +)) | (contextexpr + '+')
;
- contextelem: fixes | assumes | defines | notes | includes
+ contextelem: fixes | constrains | assumes | defines | notes | includes
;
fixes: 'fixes' (name ('::' type)? structmixfix? + 'and')
;
+ constrains: 'constrains' (name '::' type + 'and')
+ ;
assumes: 'assumes' (thmdecl? props + 'and')
;
defines: 'defines' (thmdecl? prop proppat? + 'and')
@@ -168,6 +170,9 @@
declaration ``$(structure)$'' means that $x$ may be referenced
implicitly in this context.
+ \item [$\CONSTRAINS{~x::\tau}$] introduces a type constraint $\tau$
+ on the local parameter $x$.
+
\item [$\ASSUMES{a}{\vec\phi}$] introduces local premises, similar to
$\ASSUMENAME$ within a proof (cf.\ \S\ref{sec:proof-context}).
@@ -305,6 +310,15 @@
account when choosing attributes for local theorems.
\end{warn}
+\begin{warn}
+ An interpretation may subsume previous interpretations. A warning
+ is issued, since it is likely that these could have been generalized
+ in the first place. The locale package does not attempt to remove
+ subsumed interpretations. This situation is normally harmless, but
+ note that $blast$ gets confused by the presence of multiple axclass
+ instances a rule.
+\end{warn}
+
\section{Derived proof schemes}