author wenzelm Mon, 30 Aug 1999 20:30:21 +0200 changeset 7396 d3f231fe725c parent 7395 66a3d3bb28e4 child 7397 9228085a25df
OF: "_" as argument;
--- 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
+  the reversed order).  Note that premises may be skipped by including $\_$
+  $RS$ resolves with the $n$-th premise of $thm$; $COMP$ is a version of $RS$
\item [$of~ts$ and $where~\vec x = \vec t$] perform positional and named