doc-src/IsarRef/generic.tex

 \cite{Wenzel:1997:TPHOL}.  There is also a tutorial on using axiomatic type
 classes in isabelle \cite{isabelle-axclass} that is part of the standard
 Isabelle documentation.
 
 \begin{rail}
-  'axclass' classdecl (axmdecl prop comment? +)
-  ;
-  'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity) comment?
+  'axclass' classdecl (axmdecl prop +)
+  ;
+  'instance' (nameref ('<' | subseteq) nameref | nameref '::' simplearity)
   ;
 \end{rail}
 
 \begin{descr}
 \item [$\AXCLASS~c \subseteq \vec c~axms$] defines an axiomatic type class as

 claim.  According to the nature of existential reasoning, assumptions get
 eliminated from any result exported from the context later, provided that the
 corresponding parameters do \emph{not} occur in the conclusion.
 
 \begin{rail}
-  'obtain' (vars + 'and') comment? \\ 'where' (props comment? + 'and')
+  'obtain' (vars + 'and') 'where' (props + 'and')
   ;
 \end{rail}
 
 $\OBTAINNAME$ is defined as a derived Isar command as follows, where $\vec b$
 shall refer to (optional) facts indicated for forward chaining.

   \MOREOVER & \equiv & \NOTE{calculation}{calculation~this} \\
   \ULTIMATELY & \equiv & \MOREOVER~\FROM{calculation} \\
 \end{matharray}
 
 \begin{rail}
-  ('also' | 'finally') transrules? comment?
-  ;
-  ('moreover' | 'ultimately') comment?
+  ('also' | 'finally') transrules?
   ;
   'trans' (() | 'add' | 'del')
   ;
 
-  transrules: '(' thmrefs ')' interest?
+  transrules: '(' thmrefs ')'
   ;
 \end{rail}
 
 \begin{descr}
 \item [$\ALSO~(\vec a)$] maintains the auxiliary $calculation$ register as

   ``$\FINALLY~\HAVE{}{\phi}~\DOT$'' are typical idioms for concluding
   calculational proofs.
 
 \item [$\MOREOVER$ and $\ULTIMATELY$] are analogous to $\ALSO$ and $\FINALLY$,
   but collect results only, without applying rules.
-
-\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity
-  rules declared in the current context.
+  
+\item [$\isarkeyword{print_trans_rules}$] prints the list of transitivity (and
+  symmetry) rules declared in the current context.
 
 \item [$trans$] declares theorems as transitivity rules.
 
 \end{descr}