equal
deleted
inserted
replaced
2741 \textit{Nitpick.register\_} functions can cause havoc if used improperly. |
2741 \textit{Nitpick.register\_} functions can cause havoc if used improperly. |
2742 |
2742 |
2743 \item[$\bullet$] Although this has never been observed, arbitrary theorem |
2743 \item[$\bullet$] Although this has never been observed, arbitrary theorem |
2744 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples. |
2744 morphisms could possibly confuse Nitpick, resulting in spurious counterexamples. |
2745 |
2745 |
2746 %\item[$\bullet$] All constants and types whose names start with |
2746 \item[$\bullet$] All constants, types, free variables, and schematic variables |
2747 %\textit{Nitpick}{.} are reserved for internal use. |
2747 whose names start with \textit{Nitpick}{.} are reserved for internal use. |
2748 \end{enum} |
2748 \end{enum} |
2749 |
2749 |
2750 \let\em=\sl |
2750 \let\em=\sl |
2751 \bibliography{../manual}{} |
2751 \bibliography{../manual}{} |
2752 \bibliographystyle{abbrv} |
2752 \bibliographystyle{abbrv} |