diff options
Diffstat (limited to 'doc/tutorial')
| -rwxr-xr-x | doc/tutorial/Tutorial.tex | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/doc/tutorial/Tutorial.tex b/doc/tutorial/Tutorial.tex index 55ef730a5..de3d9c3f2 100755 --- a/doc/tutorial/Tutorial.tex +++ b/doc/tutorial/Tutorial.tex @@ -1554,7 +1554,7 @@ SearchHead le. \end{coq_example} A new and more convenient search tool is \textsf{SearchPattern} -developed by Yves Bertot. It allows to find the theorems with a +developed by Yves Bertot. It allows finding the theorems with a conclusion matching a given pattern, where \verb:\_: can be used in place of an arbitrary term. We remark in this example, that \Coq{} provides usual infix notations for arithmetic operators. |