376 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}. |
376 \item[$\bullet$] \qtybf{bool\/}: \textit{true} or \textit{false}. |
377 \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or |
377 \item[$\bullet$] \qtybf{bool\_or\_smart\/}: \textit{true}, \textit{false}, or |
378 \textit{smart}. |
378 \textit{smart}. |
379 \item[$\bullet$] \qtybf{int\/}: An integer. |
379 \item[$\bullet$] \qtybf{int\/}: An integer. |
380 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}. |
380 \item[$\bullet$] \qtybf{int\_or\_smart\/}: An integer or \textit{smart}. |
381 \item[$\bullet$] \qtybf{time}: An integer followed by $\textit{min}$ (minutes), |
381 \item[$\bullet$] \qtybf{time}: An integer (e.g., 60) or floating-point number |
382 $s$ (seconds), or \textit{ms} |
382 (e.g., 0.5) expressing a number of seconds, or the keyword \textit{none} |
383 (milliseconds), or the keyword \textit{none} ($\infty$ years). |
383 ($\infty$ seconds). |
384 \end{enum} |
384 \end{enum} |
385 |
385 |
386 Default values are indicated in square brackets. Boolean options have a negated |
386 Default values are indicated in square brackets. Boolean options have a negated |
387 counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting |
387 counterpart (e.g., \textit{blocking} vs.\ \textit{non\_blocking}). When setting |
388 Boolean options, ``= \textit{true}'' may be omitted. |
388 Boolean options, ``= \textit{true}'' may be omitted. |
455 Legacy alias for \textit{provers}. |
455 Legacy alias for \textit{provers}. |
456 |
456 |
457 \opnodefault{atp}{string} |
457 \opnodefault{atp}{string} |
458 Legacy alias for \textit{provers}. |
458 Legacy alias for \textit{provers}. |
459 |
459 |
460 \opdefault{timeout}{time}{$\mathbf{30}$ s} |
460 \opdefault{timeout}{time}{$\mathbf{30}$} |
461 Specifies the maximum amount of time that the automatic provers should spend |
461 Specifies the maximum number of seconds that the automatic provers should spend |
462 searching for a proof. For historical reasons, the default value of this option |
462 searching for a proof. For historical reasons, the default value of this option |
463 can be overridden using the option ``Sledgehammer: Time Limit'' from the |
463 can be overridden using the option ``Sledgehammer: Time Limit'' from the |
464 ``Isabelle'' menu in Proof General. |
464 ``Isabelle'' menu in Proof General. |
465 |
465 |
466 \opfalse{blocking}{non\_blocking} |
466 \opfalse{blocking}{non\_blocking} |