equal
deleted
inserted
replaced
38 counter-example counter-examples data-type data-types co-data-type |
38 counter-example counter-examples data-type data-types co-data-type |
39 co-data-types in-duc-tive co-in-duc-tive} |
39 co-data-types in-duc-tive co-in-duc-tive} |
40 |
40 |
41 \urlstyle{tt} |
41 \urlstyle{tt} |
42 |
42 |
|
43 \renewcommand\_{\hbox{\textunderscore\kern-.05ex}} |
|
44 |
43 \begin{document} |
45 \begin{document} |
44 |
46 |
45 %%% TYPESETTING |
47 %%% TYPESETTING |
46 %\renewcommand\labelitemi{$\bullet$} |
48 %\renewcommand\labelitemi{$\bullet$} |
47 \renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} |
49 \renewcommand\labelitemi{\raise.065ex\hbox{\small\textbullet}} |
125 in.\allowbreak tum.\allowbreak de}} |
127 in.\allowbreak tum.\allowbreak de}} |
126 |
128 |
127 To run Nitpick, you must also make sure that the theory \textit{Nitpick} is |
129 To run Nitpick, you must also make sure that the theory \textit{Nitpick} is |
128 imported---this is rarely a problem in practice since it is part of |
130 imported---this is rarely a problem in practice since it is part of |
129 \textit{Main}. The examples presented in this manual can be found |
131 \textit{Main}. The examples presented in this manual can be found |
130 in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_Examples/Manual\_Nits.thy} theory. |
132 in Isabelle's \texttt{src/HOL/\allowbreak Nitpick\_\allowbreak Examples/\allowbreak Manual\_Nits.thy} theory. |
131 The known bugs and limitations at the time of writing are listed in |
133 The known bugs and limitations at the time of writing are listed in |
132 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning either |
134 \S\ref{known-bugs-and-limitations}. Comments and bug reports concerning either |
133 the tool or the manual should be directed to the author at \authoremail. |
135 the tool or the manual should be directed to the author at \authoremail. |
134 |
136 |
135 \vskip2.5\smallskipamount |
137 \vskip2.5\smallskipamount |