Multiple subgoals working.
authorquigley
Fri Jun 17 16:18:49 2005 +0200 (2005-06-17)
changeset 164185d0d24bd2c96
parent 16417 9bc16273c2d4
child 16419 0c3db621bbbd
Multiple subgoals working.
src/HOL/Tools/ATP/recon_parse.ML
src/HOL/Tools/ATP/recon_translate_proof.ML
     1.1 --- a/src/HOL/Tools/ATP/recon_parse.ML	Fri Jun 17 16:12:49 2005 +0200
     1.2 +++ b/src/HOL/Tools/ATP/recon_parse.ML	Fri Jun 17 16:18:49 2005 +0200
     1.3 @@ -135,8 +135,20 @@
     1.4  \\
     1.5  \--------------------------SPASS-STOP------------------------------"
     1.6  
     1.7 +fun extract_proof s
     1.8 +      = if cut_exists "Here is a proof with" s then
     1.9 +          (kill_lines 0
    1.10 +           o snd o cut_after ":"
    1.11 +           o snd o cut_after "Here is a proof with"
    1.12 +           o fst o cut_after " ||  -> .") s
    1.13 +        else if cut_exists "%================== Proof: ======================" s then
    1.14 +          (kill_lines 0
    1.15 +           o snd o cut_after "%================== Proof: ======================"
    1.16 +           o fst o cut_before "==============  End of proof. ==================") s
    1.17 +        else
    1.18 +          raise SPASSError "Couldn't find a proof."
    1.19  
    1.20 -fun extract_proof s
    1.21 +(*fun extract_proof s
    1.22        = if cut_exists "Here is a proof with" s then
    1.23            (kill_lines 0
    1.24             o snd o cut_after ":"
    1.25 @@ -144,7 +156,7 @@
    1.26             o fst o cut_after " ||  -> .") s
    1.27          else
    1.28            raise SPASSError "Couldn't find a proof."
    1.29 -
    1.30 +*)
    1.31  
    1.32  
    1.33  fun several p = many (some p)
     2.1 --- a/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Jun 17 16:12:49 2005 +0200
     2.2 +++ b/src/HOL/Tools/ATP/recon_translate_proof.ML	Fri Jun 17 16:18:49 2005 +0200
     2.3 @@ -28,8 +28,9 @@
     2.4  
     2.5  datatype Side = Left |Right
     2.6  
     2.7 - datatype Proofstep = ExtraAxiom
     2.8 -                     |OrigAxiom
     2.9 + datatype Proofstep =  ExtraAxiom
    2.10 +                     | OrigAxiom
    2.11 +  		     | VampInput 
    2.12                       | Axiom
    2.13                       | Binary of (int * int) * (int * int)   (* (clause1,lit1), (clause2, lit2) *)
    2.14                       | MRR of (int * int) * (int * int)