| products/sources/formale Sprachen/Coq/theories/Compat/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: argo_expr.ML Sprache: IsabelleOriginal von: Isabelle© |
|
||||||
|
(* :mode=isabelle-options: *)
section "Automatically tried tools" public option auto_time_start : real = 1.0 -- "initial delay for automatically tried tools (seconds)" public option auto_time_limit : real = 2.0 -- "time limit for automatically tried tools (seconds > 0)" public option auto_nitpick : bool = false -- "run Nitpick automatically" public option auto_sledgehammer : bool = false -- "run Sledgehammer automatically" public option auto_methods : bool = false -- "try standard proof methods automatically" public option auto_quickcheck : bool = true -- "run Quickcheck automatically" public option auto_solve_direct : bool = true -- "run solve_direct automatically" section "Miscellaneous Tools" public option sledgehammer_provers : string = "cvc4 z3 spass e remote_vampire" -- "provers for Sledgehammer (separated by blanks)" public option sledgehammer_timeout : int = 30 -- "provers will be interrupted after this time (in seconds)" public option vampire_noncommercial : string = "unknown" -- "status of Vampire activation for noncommercial use (yes, no, unknown)" public option MaSh : string = "sml" -- "machine learning algorithm to use by Sledgehammer (nb_knn, nb, knn, none)" public option kodkod_scala : bool = true -- "invoke Nitpick/Kodkod via Isabelle/Scala (instead of external process)" public option kodkod_max_threads : int = 0 -- "default max_threads for Nitpick/Kodkod (0: maximum of Java/Scala platform)" ¤ Dauer der Verarbeitung: 0.4 Sekunden (vorverarbeitet) ¤ |
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.Die farbliche Syntaxdarstellung ist noch experimentell.Bot Zugriff |
