diff options
Diffstat (limited to 'doc/refman/RefMan-tacex.tex')
| -rw-r--r-- | doc/refman/RefMan-tacex.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/refman/RefMan-tacex.tex b/doc/refman/RefMan-tacex.tex index 6667fd5a4..5703c73f0 100644 --- a/doc/refman/RefMan-tacex.tex +++ b/doc/refman/RefMan-tacex.tex @@ -345,7 +345,7 @@ Reset Initial. \section[\tt quote]{\tt quote\tacindex{quote} \label{quote-examples}} -The tactic \texttt{quote} allows to use Barendregt's so-called +The tactic \texttt{quote} allows using Barendregt's so-called 2-level approach without writing any ML code. Suppose you have a language \texttt{L} of 'abstract terms' and a type \texttt{A} of 'concrete terms' |