Lines Matching refs:method
121 proof typically relies on the general-purpose \textit{metis} proof method, which
268 \textit{smt} method call. Rough timings are shown in parentheses, indicating how
468 The \textit{metis}~(\textit{full\_types}) proof method
473 higher-order places (e.g., in set comprehensions). The method is automatically
516 a given prover and repeatedly calls a prover or proof method with subsets of
649 The \textit{metis} proof method has the syntax
1127 is the default encoding used by the \textit{metis} proof method.
1177 \textit{metis} proof method, the question mark is replaced by a
1186 \textit{metis} proof method, the `\hbox{??}' suffix is replaced by
1194 \textit{metis} proof method, the `\hbox{@}' suffix is replaced by
1261 Specifies whether the \textit{smt} proof method should be tried in addition to
1263 default), the \textit{smt} method is used for one-line proofs but not in Isar
1303 next to the suggested proof method calls.