updated docs
Tue, 04 Mar 2014 18:57:17 +0100
changeset 55902 39cc8409373f
parent 55901 8c6d49dd8ae1
child 55903 461a75d00323
updated docs
--- a/src/Doc/Nitpick/document/root.tex	Tue Mar 04 18:57:17 2014 +0100
+++ b/src/Doc/Nitpick/document/root.tex	Tue Mar 04 18:57:17 2014 +0100
@@ -2765,21 +2765,13 @@
 ignored. Again, such nonconservative extensions are generally considered bad
-\item[\labelitemi] Nitpick maintains a global cache of wellfoundedness conditions,
-which can become invalid if you change the definition of an inductive predicate
-that is registered in the cache. To clear the cache,
-run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
 \item[\labelitemi] Nitpick produces spurious counterexamples when invoked after a
 \textbf{guess} command in a structured proof.
-\item[\labelitemi] Datatypes defined using \textbf{datatype\_new} are not
-\item[\labelitemi] Codatatypes defined using \textbf{codatatype} that
-involve nested recursion through non-codatatypes are not properly supported
-and may result in spurious counterexamples.
+\item[\labelitemi] Datatypes defined using \textbf{datatype\_new} and
+codatatypes defined using \textbf{codatatype} that involve nested (co)recursion
+through non-(co)datatypes are not properly supported and may result in spurious
 \item[\labelitemi] The \textit{nitpick\_xxx} attributes and the
 \textit{Nitpick\_xxx.register\_yyy} functions can cause havoc if used