# HG changeset patch
# User blanchet
# Date 1298285437 -3600
# Node ID 03bf23a265b683ae978898747601addb71090faa
# Parent  c7a2669ae75dc14f4a2574c0a7a1d4be98746d7a
updated docs

diff -r c7a2669ae75d -r 03bf23a265b6 doc-src/Nitpick/nitpick.tex
--- a/doc-src/Nitpick/nitpick.tex	Mon Feb 21 11:50:31 2011 +0100
+++ b/doc-src/Nitpick/nitpick.tex	Mon Feb 21 11:50:37 2011 +0100
@@ -2543,6 +2543,10 @@
 alternative definition should be logically equivalent to the constant's actual
 axiomatic definition and should be of the form
 
+\qquad $c~{?}x_1~\ldots~{?}x_n \,=\, t$,
+
+or
+
 \qquad $c~{?}x_1~\ldots~{?}x_n \,\equiv\, t$,
 
 where ${?}x_1, \ldots, {?}x_n$ are distinct variables and $c$ does not occur in