equal
deleted
inserted
replaced
114 You can also invoke Nitpick from the ``Commands'' submenu of the |
114 You can also invoke Nitpick from the ``Commands'' submenu of the |
115 ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c C-a |
115 ``Isabelle'' menu in Proof General or by pressing the Emacs key sequence C-c C-a |
116 C-n. This is equivalent to entering the \textbf{nitpick} command with no |
116 C-n. This is equivalent to entering the \textbf{nitpick} command with no |
117 arguments in the theory text. |
117 arguments in the theory text. |
118 |
118 |
119 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.6 virtual |
119 Nitpick requires the Kodkodi package for Isabelle as well as a Java 1.5 virtual |
120 machine called \texttt{java}. The examples presented in this manual can be found |
120 machine called \texttt{java}. The examples presented in this manual can be found |
121 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory. |
121 in Isabelle's \texttt{src/HOL/Nitpick\_Examples/Manual\_Nits.thy} theory. |
122 |
122 |
123 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command. |
123 Throughout this manual, we will explicitly invoke the \textbf{nitpick} command. |
124 Nitpick also provides an automatic mode that can be enabled using the |
124 Nitpick also provides an automatic mode that can be enabled using the |