src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
changeset 60318 ab785001b51d
parent 59882 ada832308efe
child 60319 127c2f00ca94
     1.1 --- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat May 30 22:18:12 2015 +0200
     1.2 +++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Sat May 30 23:30:54 2015 +0200
     1.3 @@ -1930,7 +1930,7 @@
     1.4                       ORELSE' atac
     1.5                       ORELSE' kill_meta_eqs_tac)
     1.6  
     1.7 -    val tectic =
     1.8 +    val tactic =
     1.9        (rtac @{thm polarise} 1 THEN atac 1)
    1.10        ORELSE
    1.11          (REPEAT_DETERM (etac @{thm conjE} 1 THEN etac @{thm drop_first_hypothesis} 1)
    1.12 @@ -1944,7 +1944,7 @@
    1.13              (unfold_tac ctxt depends_on_defs
    1.14               THEN IF_UNSOLVED continue_reducing_tac)))
    1.15    in
    1.16 -    tectic st
    1.17 +    tactic st
    1.18    end
    1.19  *}
    1.20