--- a/doc-src/IsarRef/generic.tex Mon Mar 10 18:44:20 2008 +0100
+++ b/doc-src/IsarRef/generic.tex Mon Mar 10 21:51:42 2008 +0100
@@ -243,7 +243,7 @@
contextexpr: nameref | '(' contextexpr ')' |
(contextexpr (name mixfix? +)) | (contextexpr + '+')
;
- contextelem: fixes | constrains | assumes | defines | notes | includes
+ contextelem: fixes | constrains | assumes | defines | notes
;
fixes: 'fixes' ((name ('::' type)? structmixfix? | vars) + 'and')
;
@@ -559,6 +559,9 @@
$\ASSUMESNAME$ in $body$ are also lifted, mapping each local parameter
$f::\tau [\alpha]$ to its corresponding global constant
$f::\tau [?\alpha::c]$.
+ A suitable introduction rule is provided as $c_class_axioms.intro$.
+ Explicit references to this should rarely be needed; mostly
+ this rules will be applied implicitly by the $intro_classes$ method.
\item [$\INSTANTIATION~\vec t~::~(\vec s)~s~\isarkeyword{begin}$]
opens a theory target (cf.\S\ref{sec:target}) which allows to specify