--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat May 30 22:18:12 2015 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy Sat May 30 23:30:54 2015 +0200
@@ -1930,7 +1930,7 @@
ORELSE' atac
ORELSE' kill_meta_eqs_tac)
- val tectic =
+ val tactic =
(rtac @{thm polarise} 1 THEN atac 1)
ORELSE
(REPEAT_DETERM (etac @{thm conjE} 1 THEN etac @{thm drop_first_hypothesis} 1)
@@ -1944,7 +1944,7 @@
(unfold_tac ctxt depends_on_defs
THEN IF_UNSOLVED continue_reducing_tac)))
in
- tectic st
+ tactic st
end
*}