ML \<open>
val do_it = false (* switch to "true" to generate the files *)
val thys = [\<^theory>\<open>List\<close>]
val params as {provers, ...} = Sledgehammer_Commands.default_params \<^theory> []
val prover = hd provers
val range = (1, NONE)
val step = 1
val max_suggestions = 1024
val dir = "List"
val prefix = "/tmp/" ^ dir ^ "/" \<close>
end
¤ Dauer der Verarbeitung: 0.10 Sekunden
(vorverarbeitet)
¤
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.