robust handling of Vampire 4 proofs
authorblanchet
Thu Aug 27 20:16:07 2015 +0200 (2015-08-27)
changeset 61030aeb578badc1c
parent 61029 b09461b3bc05
child 61031 162bd20dae23
robust handling of Vampire 4 proofs
NEWS
src/HOL/Tools/ATP/atp_proof.ML
     1.1 --- a/NEWS	Thu Aug 27 20:10:40 2015 +0200
     1.2 +++ b/NEWS	Thu Aug 27 20:16:07 2015 +0200
     1.3 @@ -192,6 +192,7 @@
     1.4    - Proof reconstruction has been improved, to minimize the incidence of
     1.5      cases where Sledgehammer gives a proof that does not work.
     1.6    - Auto Sledgehammer now minimizes and preplays the results.
     1.7 +  - Handle Vampire 4.0 proof output without raising exception.
     1.8  
     1.9  * Nitpick:
    1.10    - Removed "check_potential" and "check_genuine" options.
     2.1 --- a/src/HOL/Tools/ATP/atp_proof.ML	Thu Aug 27 20:10:40 2015 +0200
     2.2 +++ b/src/HOL/Tools/ATP/atp_proof.ML	Thu Aug 27 20:16:07 2015 +0200
     2.3 @@ -404,7 +404,7 @@
     2.4  and parse_quantified_formula x =
     2.5    (($$ tptp_forall >> K AForall || $$ tptp_exists >> K AExists)
     2.6     --| $$ "[" -- parse_terms --| $$ "]" --| $$ ":" -- parse_literal
     2.7 -   >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, []), _) => (s, NONE)) ts, phi))) x
     2.8 +   >> (fn ((q, ts), phi) => AQuant (q, map (fn ATerm ((s, _), _) => (s, NONE)) ts, phi))) x
     2.9  
    2.10  val parse_tstp_extra_arguments =
    2.11    Scan.optional ($$ "," |-- parse_source --| Scan.option ($$ "," |-- skip_term)) dummy_inference