doc-src/TutorialI/Misc/document/simp.tex

 finds theorems whose name does not contain \texttt{List}. You can use this
 to exclude particular theories from the search: the long name of
 a theorem contains the name of the theory it comes from.
 
 Finallly, different search criteria can be combined arbitrarily. 
-The effect is conjuctive: Find returns the theorerms that satisfy all of
+The effect is conjuctive: Find returns the theorems that satisfy all of
 the criteria. For example,
 \begin{ttbox}
 "_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
 \end{ttbox}
 looks for theorems containing plus but not minus, and which do not simplify