summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | blanchet |

Fri, 06 Aug 2010 11:05:57 +0200 | |

changeset 38213 | d4cbc80e7271 |

parent 38212 | a7e92239922f |

child 38214 | 8164c91039ea |

extend the scope of limitation about nonconservative extensions

--- a/doc-src/Nitpick/nitpick.tex Fri Aug 06 10:50:52 2010 +0200 +++ b/doc-src/Nitpick/nitpick.tex Fri Aug 06 11:05:57 2010 +0200 @@ -2864,16 +2864,19 @@ \textbf{by}~(\textit{auto simp}:~\textit{prec\_def}) \postw -Such theorems are considered bad style because they rely on the internal -representation of functions synthesized by Isabelle, which is an implementation +Such theorems are generally considered bad style because they rely on the +internal representation of functions synthesized by Isabelle, an implementation detail. \item[$\bullet$] Similarly, Nitpick might find spurious counterexamples for theorems that rely on the use of the indefinite description operator internally by \textbf{specification} and \textbf{quot\_type}. -\item[$\bullet$] Axioms that restrict the possible values of the -\textit{undefined} constant are in general ignored. +\item[$\bullet$] Axioms or definitions that restrict the possible values of the +\textit{undefined} constant or other partially specified built-in Isabelle +constants (e.g., \textit{Abs\_} and \textit{Rep\_} constants) are in general +ignored. Again, such nonconservative extensions are generally considered bad +style. \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions, which can become invalid if you change the definition of an inductive predicate