changeset 7175 | 8263d0b50e12 |
parent 7167 | 0b2e3ef1d8f4 |
child 7315 | 76a39a3784b5 |
--- a/doc-src/IsarRef/generic.tex Wed Aug 04 18:20:05 1999 +0200 +++ b/doc-src/IsarRef/generic.tex Wed Aug 04 18:20:24 1999 +0200 @@ -53,13 +53,19 @@ \begin{rail} ('tag' | 'untag') (nameref+) ; +\end{rail} + +\begin{rail} ('COMP' | 'RS') nat? thmref ; 'OF' thmrefs ; - 'where' (term '=' term * 'and') +\end{rail} + +\begin{rail} + 'where' (name '=' term * 'and') ; - 'of' (inst * ) ('concl:' (inst * ))? + 'of' (inst * ) ('concl' ':' (inst * ))? ; inst: underscore | term