# HG changeset patch
# User wenzelm
# Date 936037821 -7200
# Node ID d3f231fe725c25e12f2e4332606b21c067a1bc37
# Parent  66a3d3bb28e407180fe68df6b659d129f99a581a
OF: "_" as argument;

diff -r 66a3d3bb28e4 -r d3f231fe725c doc-src/IsarRef/generic.tex
--- a/doc-src/IsarRef/generic.tex	Mon Aug 30 20:29:28 1999 +0200
+++ b/doc-src/IsarRef/generic.tex	Mon Aug 30 20:30:21 1999 +0200
@@ -100,9 +100,12 @@
   result).
 \item [$OF~thms$, $RS~n~thm$, and $COMP~n~thm$] compose rules.  $OF$ applies
   $thms$ in parallel (cf.\ \texttt{MRS} in \cite[\S5]{isabelle-ref}, but note
-  the reversed order).  $RS$ resolves with the $n$-th premise of $thm$; $COMP$
-  is a version of $RS$ that does not include the automatic lifting process
-  that is normally intended (see also \texttt{RS} and \texttt{COMP} in
+  the reversed order).  Note that premises may be skipped by including $\_$
+  (underscore) as argument.
+  
+  $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
+  that does not include the automatic lifting process that is normally
+  intended (see also \texttt{RS} and \texttt{COMP} in
   \cite[\S5]{isabelle-ref}).
   
 \item [$of~ts$ and $where~\vec x = \vec t$] perform positional and named