doc-src/Nitpick/nitpick.tex
changeset 33559 63925777ccf9
parent 33557 107f3df799f6
child 33561 ab01b72715ef
equal deleted inserted replaced
33558:a2db56854b83 33559:63925777ccf9
  2465 
  2465 
  2466 Such theorems are considered bad style because they rely on the internal
  2466 Such theorems are considered bad style because they rely on the internal
  2467 representation of functions synthesized by Isabelle, which is an implementation
  2467 representation of functions synthesized by Isabelle, which is an implementation
  2468 detail.
  2468 detail.
  2469 
  2469 
  2470 \item[$\bullet$] Nitpick maintains a global cache of wellformedness conditions,
  2470 \item[$\bullet$] Nitpick maintains a global cache of wellfoundedness conditions,
  2471 which can become invalid if you change the definition of an inductive predicate
  2471 which can become invalid if you change the definition of an inductive predicate
  2472 that is registered in the cache. To clear the cache,
  2472 that is registered in the cache. To clear the cache,
  2473 run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
  2473 run Nitpick with the \textit{tac\_timeout} option set to a new value (e.g.,
  2474 501$\,\textit{ms}$).
  2474 501$\,\textit{ms}$).
  2475 
  2475