# HG changeset patch
# User wenzelm
# Date 1433021454 -7200
# Node ID ab785001b51d4cde4c7e045cabd4d4b708d5e745
# Parent  9b7248379101eb6362b247b6ef30e7c2f4596426
tuned spelling;

diff -r 9b7248379101 -r ab785001b51d src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- 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
 *}