doc-src/Nitpick/nitpick.tex

 This attribute specifies the equations that constitute the specification of a
 constant. For functions defined using the \textbf{primrec}, \textbf{function},
 and \textbf{nominal\_\allowbreak primrec} packages, this corresponds to the
 \textit{simps} rules. The equations must be of the form
 
-\qquad $c~t_1~\ldots\ t_n \;\bigl[{=}\; u\bigr].$
+\qquad $c~t_1~\ldots\ t_n \;\bigl[{=}\; u\bigr]$
+
+or
+
+\qquad $c~t_1~\ldots\ t_n \,\equiv\, u.$
 
 \flushitem{\textit{nitpick\_psimp}}
 
 \nopagebreak
 This attribute specifies the equations that constitute the partial specification
 of a constant. For functions defined using the \textbf{function} package, this
 corresponds to the \textit{psimps} rules. The conditional equations must be of
 the form
 
-\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \;\bigl[{=}\; u\bigr]$.
+\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \;\bigl[{=}\; u\bigr]$
+
+or
+
+\qquad $\lbrakk P_1;\> \ldots;\> P_m\rbrakk \,\Longrightarrow\, c\ t_1\ \ldots\ t_n \,\equiv\, u$.
 
 \flushitem{\textit{nitpick\_choice\_spec}}
 
 \nopagebreak
 This attribute specifies the (free-form) specification of a constant defined

 
 \qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{lfp}~(\lambda f.\; t)$
 
 or
 
-\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{gfp}~(\lambda f.\; t)$
+\qquad $c~{?}x_1~\ldots~{?}x_m \,\equiv\, \lambda y_1~\ldots~y_n.\; \textit{gfp}~(\lambda f.\; t).$
 
 Nitpick assumes that the definition was made using a (co)inductive package
 based on the user-specified introduction rules registered in Isabelle's internal
 \textit{Spec\_Rules} table. The tool uses the introduction rules to ascertain
 whether the definition is well-founded and the definition to generate a