src/HOL/Tools/ATP/atp_systems.ML
changeset 38817 bf27c24ba224
parent 38744 2b6333f78a9e
child 38997 78ac4468cf9d
equal deleted inserted replaced
38816:21a6f261595e 38817:bf27c24ba224
   291                  use_conjecture_for_hypotheses)
   291                  use_conjecture_for_hypotheses)
   292 fun remotify_prover (name, config) system_name system_versions =
   292 fun remotify_prover (name, config) system_name system_versions =
   293   (remotify_name name, remotify_config system_name system_versions config)
   293   (remotify_name name, remotify_config system_name system_versions config)
   294 
   294 
   295 val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
   295 val remote_e = remotify_prover e "EP" ["1.0", "1.1", "1.2"]
   296 val remote_vampire = remotify_prover vampire "Vampire" ["9.9", "0.6", "1.0"]
   296 val remote_vampire = remotify_prover vampire "Vampire" ["9.0", "1.0", "0.6"]
   297 val remote_sine_e =
   297 val remote_sine_e =
   298   remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
   298   remote_prover "sine_e" "SInE" [] [] [(Unprovable, "says Unknown")]
   299                 1000 (* FUDGE *) false true
   299                 1000 (* FUDGE *) false true
   300 val remote_snark =
   300 val remote_snark =
   301   remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []
   301   remote_prover "snark" "SNARK---" [] [("refutation.", "end_refutation.")] []