# HG changeset patch
# User haftmann
# Date 1205182302 -3600
# Node ID 0686a953b87327265973ee5506077c4d26b4526f
# Parent  69592314f9773bdd320e24e7b22004c8a37708e3
adjusted to current implementation

diff -r 69592314f977 -r 0686a953b873 doc-src/IsarRef/generic.tex
--- 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