doc-src/TutorialI/Misc/document/simp.tex
 changeset 20144 2517cd4b1f37 parent 17187 45bee2f6e61f child 20212 f4a8b4e2fb29
equal inserted replaced
20143:54e493016486 20144:2517cd4b1f37
   733 finds theorems whose name does not contain \texttt{List}. You can use this
   733 finds theorems whose name does not contain \texttt{List}. You can use this
   734 to exclude particular theories from the search: the long name of
   734 to exclude particular theories from the search: the long name of
   735 a theorem contains the name of the theory it comes from.
   735 a theorem contains the name of the theory it comes from.
   736
   736
   737 Finallly, different search criteria can be combined arbitrarily.
   737 Finallly, different search criteria can be combined arbitrarily.
   738 The effect is conjuctive: Find returns the theorerms that satisfy all of
   738 The effect is conjuctive: Find returns the theorems that satisfy all of
   739 the criteria. For example,
   739 the criteria. For example,
   740 \begin{ttbox}
   740 \begin{ttbox}
   741 "_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
   741 "_ + _"  -"_ - _"  -simp: "_ * (_ + _)"  name: assoc
   742 \end{ttbox}
   742 \end{ttbox}
   743 looks for theorems containing plus but not minus, and which do not simplify
   743 looks for theorems containing plus but not minus, and which do not simplify