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