Update refman's Search documentation

doc/sphinx/proof-engine/vernacular-commands.rst

@@ -198,8 +198,8 @@ described elsewhere
       Filters objects by the keyword that was used to define them
       (`Theorem`, `Lemma`, `Axiom`, `Variable`, `Context`,
       `Primitive`...) or its status (`Coercion`, `Instance`, `Scheme`,
-      `Canonical`, `SubClass`, Field` for record fields, `Method` for class
-      fields).  Note that `Coercion`\s, `Canonical Structure`\s, Instance`\s and `Scheme`\s can be
+      `Canonical`, `SubClass`, `Field` for record fields, `Method` for class
+      fields).  Note that `Coercion`\s, `Canonical Structure`\s, `Instance`\s and `Scheme`\s can be
       defined without using those keywords.  See :ref:`this example <search-by-keyword>`.
 
    Additional clauses:
@@ -308,6 +308,13 @@ described elsewhere
 
          Search is:Instance [ Reflexive | Symmetric ].
 
+      The following search outputs operations on `nat` defined in the
+      prelude either with the `Definition` or `Fixpoint` keyword:
+
+      .. coqtop:: all reset
+
+         Search (nat -> nat -> nat) -bool [ is:Definition | is:Fixpoint ].
+
 .. cmd:: SearchPattern @one_pattern {? {| inside | in | outside } {+ @qualid } }
 
    Displays the name and type of all hypotheses of the