src/HOL/Tools/ATP/atp_systems.ML
changeset 43288 7a4eebdebb23
parent 43221 2c88166938eb
child 43354 396aaa15dd8b
equal deleted inserted replaced
43274:ad4611809a29 43288:7a4eebdebb23
   430   remote_atp waldmeisterN "Waldmeister" ["710"]
   430   remote_atp waldmeisterN "Waldmeister" ["710"]
   431              [("#START OF PROOF", "Proved Goals:")]
   431              [("#START OF PROOF", "Proved Goals:")]
   432              [(OutOfResources, "Too many function symbols"),
   432              [(OutOfResources, "Too many function symbols"),
   433               (Crashed, "Unrecoverable Segmentation Fault")]
   433               (Crashed, "Unrecoverable Segmentation Fault")]
   434              Hypothesis Hypothesis [CNF_UEQ]
   434              Hypothesis Hypothesis [CNF_UEQ]
   435              (K (50, ["poly_args"]) (* FUDGE *))
   435              (K (50, ["mangled_args", "mangled_tags?"]) (* FUDGE *))
   436 
   436 
   437 (* Setup *)
   437 (* Setup *)
   438 
   438 
   439 fun add_atp (name, config) thy =
   439 fun add_atp (name, config) thy =
   440   Data.map (Symtab.update_new (name, (config, stamp ()))) thy
   440   Data.map (Symtab.update_new (name, (config, stamp ()))) thy