Metis is being used to emulate E steps;
authorsultana
Sun Jun 22 06:16:57 2014 +0100 (2014-06-22)
changeset 577732719eb9d40fe
parent 57772 7d9134b032b2
child 57774 d2ad1320c770
Metis is being used to emulate E steps;
src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jun 22 06:16:56 2014 +0100
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sun Jun 22 06:16:57 2014 +0100
     1.3 @@ -2116,7 +2116,10 @@
     1.4    in
     1.5      case inference_name of
     1.6        "fo_atp_e" =>
     1.7 +        HEADGOAL (Metis_Tactic.metis_tac [] ATP_Problem_Generate.combs_or_liftingN ctxt [])
     1.8 +        (*NOTE To treat E as an oracle use the following line:
     1.9          HEADGOAL (etac (oracle_based_reconstruction_tac ctxt prob_name node))
    1.10 +        *)
    1.11      | "copy" =>
    1.12           HEADGOAL
    1.13            (atac
    1.14 @@ -2284,4 +2287,4 @@
    1.15    end
    1.16  *}
    1.17  
    1.18 -end
    1.19 \ No newline at end of file
    1.20 +end