src/HOL/TPTP/TPTP_Parser_Example.thy
changeset 53393 5278312037f8
parent 48891 c0eafbd55de3
child 55049 327eafb594ba
     1.1 --- a/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Sep 03 21:46:41 2013 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Parser_Example.thy	Tue Sep 03 21:46:41 2013 +0100
     1.3 @@ -10,7 +10,7 @@
     1.4  
     1.5  ML_file "sledgehammer_tactics.ML"
     1.6  
     1.7 -import_tptp "$TPTP/Problems/CSR/CSR077+1.p"
     1.8 +import_tptp "$TPTP/Problems/LCL/LCL414+1.p"
     1.9  
    1.10  ML {*
    1.11  val an_fmlas =
    1.12 @@ -46,7 +46,7 @@
    1.13    let
    1.14      val assumptions =
    1.15        extract_terms
    1.16 -       [TPTP_Syntax.Role_Definition (*FIXME include axioms, etc here*)]
    1.17 +       [TPTP_Syntax.Role_Definition, TPTP_Syntax.Role_Axiom]
    1.18         an_fmlas
    1.19        |> map snd
    1.20      val goals = extract_terms [TPTP_Syntax.Role_Conjecture] an_fmlas
    1.21 @@ -61,9 +61,13 @@
    1.22    {add = [], del = [], only = false} 1)
    1.23  *}
    1.24  
    1.25 -ML "auto_prove @{context} an_fmlas"
    1.26 +ML {*
    1.27 +@{assert} (is_some (try (auto_prove @{context}) an_fmlas) = false)
    1.28 +*}
    1.29  
    1.30 -sledgehammer_params [provers = z3_tptp leo2, debug]
    1.31 -ML "sh_prove @{context} an_fmlas"
    1.32 +sledgehammer_params [provers = remote_z3, debug]
    1.33 +ML {*
    1.34 +@{assert} (is_some (try (sh_prove @{context}) an_fmlas) = true)
    1.35 +*}
    1.36  
    1.37  end
    1.38 \ No newline at end of file