diff -r 143f58bb34f9 -r 0909deb8059b src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Thu May 26 16:57:14 2016 +0200
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction_Test_Units.thy	Thu May 26 17:51:22 2016 +0200
@@ -13,13 +13,13 @@
 declare [[tptp_trace_reconstruction = true]]
 
 lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \<Longrightarrow> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
-apply (tactic {*canonicalise_qtfr_order @{context} 1*})
+apply (tactic \<open>canonicalise_qtfr_order @{context} 1\<close>)
 oops
 
 lemma "! (X1 :: bool) (X2 :: bool) (X3 :: bool) (X4 :: bool) (X5 :: bool). P \<Longrightarrow> ! (X1 :: bool) (X3 :: bool) (X5 :: bool). P"
-apply (tactic {*canonicalise_qtfr_order @{context} 1*})
+apply (tactic \<open>canonicalise_qtfr_order @{context} 1\<close>)
 apply (rule allI)+
-apply (tactic {*nominal_inst_parametermatch_tac @{context} @{thm allE} 1*})+
+apply (tactic \<open>nominal_inst_parametermatch_tac @{context} @{thm allE} 1\<close>)+
 oops
 
 (*Could test bind_tac further with NUM667^1 inode43*)
@@ -187,35 +187,35 @@
 lemma "(A = B) = True ==> (B = A) = True"
 *)
 lemma "!!x. ((A x :: bool) = B x) = False ==> (B x = A x) = False"
-apply (tactic {*expander_animal @{context} 1*})
+apply (tactic \<open>expander_animal @{context} 1\<close>)
 oops
 
 lemma "(A & B) ==> ~(~A | ~B)"
-by (tactic {*expander_animal @{context} 1*})
+by (tactic \<open>expander_animal @{context} 1\<close>)
 
 lemma "(A | B) ==> ~(~A & ~B)"
-by (tactic {*expander_animal @{context} 1*})
+by (tactic \<open>expander_animal @{context} 1\<close>)
 
 lemma "(A | B) | C ==> A | (B | C)"
-by (tactic {*expander_animal @{context} 1*})
+by (tactic \<open>expander_animal @{context} 1\<close>)
 
 lemma "(~~A) = B ==> A = B"
-by (tactic {*expander_animal @{context} 1*})
+by (tactic \<open>expander_animal @{context} 1\<close>)
 
 lemma "~ ~ (A = True) ==> A = True"
-by (tactic {*expander_animal @{context} 1*})
+by (tactic \<open>expander_animal @{context} 1\<close>)
 
 (*This might not be a goal which might realistically arise:
 lemma "((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))" *)
 lemma "((~~A) = True) ==> ~(~(A = True) | ~(True = A))"
-apply (tactic {*expander_animal @{context} 1*})+
+apply (tactic \<open>expander_animal @{context} 1\<close>)+
 apply (rule conjI)
 apply assumption
 apply (rule sym, assumption)
 done
 
 lemma "A = B ==> ((~~A) = B) & (B = (~~A)) ==> ~(~(A = B) | ~(B = A))"
-by (tactic {*expander_animal @{context} 1*})+
+by (tactic \<open>expander_animal @{context} 1\<close>)+
 
 (*some lemmas assume constants in the signature of PUZ114^5*)
 consts
@@ -242,7 +242,7 @@
            SY30 (PUZ114_5_bnd_s Xj) (PUZ114_5_bnd_s Xk)))
      | SY30 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2
 )"
-by (tactic {*expander_animal @{context} 1*})+
+by (tactic \<open>expander_animal @{context} 1\<close>)+
 
 (*
 extcnf_forall_pos:
@@ -262,8 +262,8 @@
 (where X' is fresh, or renamings are done suitably).*)
 
 lemma "A | B \<Longrightarrow> A | B | C"
-apply (tactic {*flip_conclusion_tac @{context} 1*})+
-apply (tactic {*break_hypotheses 1*})+
+apply (tactic \<open>flip_conclusion_tac @{context} 1\<close>)+
+apply (tactic \<open>break_hypotheses 1\<close>)+
 oops
 
 consts
@@ -297,7 +297,7 @@
                 True) =
                False"
 apply (rule allI, erule_tac x = "SV2" in allE)
-apply (tactic {*extuni_dec_tac @{context} 1*})
+apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
 done
 
 (*SEU882^5*)
@@ -330,12 +330,12 @@
 
 lemma "A | B \<Longrightarrow> C1 | A | C2 | B | C3"
 apply (erule disjE)
-apply (tactic {*clause_breaker 1*})
-apply (tactic {*clause_breaker 1*})
+apply (tactic \<open>clause_breaker 1\<close>)
+apply (tactic \<open>clause_breaker 1\<close>)
 done
 
 lemma "A \<Longrightarrow> A"
-apply (tactic {*clause_breaker 1*})
+apply (tactic \<open>clause_breaker 1\<close>)
 done
 
 typedecl NUM667_1_bnd_nat
@@ -359,15 +359,15 @@
         NUM667_1_bnd_less SV9 SV10 = True) \<or>
        (SV9 = SV11) =
        False"
-apply (tactic {*strip_qtfrs_tac @{context}*})
-apply (tactic {*break_hypotheses 1*})
-apply (tactic {*ALLGOALS (TRY o clause_breaker)*})
-apply (tactic {*extuni_dec_tac @{context} 1*})
+apply (tactic \<open>strip_qtfrs_tac @{context}\<close>)
+apply (tactic \<open>break_hypotheses 1\<close>)
+apply (tactic \<open>ALLGOALS (TRY o clause_breaker)\<close>)
+apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
 done
 
-ML {*
+ML \<open>
 extuni_dec_n @{context} 2;
-*}
+\<close>
 
 (*NUM667^1, node 202*)
 lemma "\<forall>SV9 SV10 SV11.
@@ -382,10 +382,10 @@
         NUM667_1_bnd_less SV9 SV10 = True) \<or>
        NUM667_1_bnd_less NUM667_1_bnd_x NUM667_1_bnd_y =
        True"
-apply (tactic {*strip_qtfrs_tac @{context}*})
-apply (tactic {*break_hypotheses 1*})
-apply (tactic {*ALLGOALS (TRY o clause_breaker)*})
-apply (tactic {*extuni_dec_tac @{context} 1*})
+apply (tactic \<open>strip_qtfrs_tac @{context}\<close>)
+apply (tactic \<open>break_hypotheses 1\<close>)
+apply (tactic \<open>ALLGOALS (TRY o clause_breaker)\<close>)
+apply (tactic \<open>extuni_dec_tac @{context} 1\<close>)
 done
 
 (*NUM667^1 node 141*)
@@ -400,7 +400,7 @@
 done
 *)
 
-ML {*
+ML \<open>
 fun full_extcnf_combined_tac ctxt =
   extcnf_combined_tac ctxt NONE
    [ConstsDiff,
@@ -418,9 +418,9 @@
     CleanUp [RemoveHypothesesFromSkolemDefs, RemoveDuplicates],
     AbsorbSkolemDefs]
    []
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun nonfull_extcnf_combined_tac ctxt feats =
   extcnf_combined_tac ctxt NONE
    [ConstsDiff,
@@ -428,7 +428,7 @@
     InnerLoopOnce (Break_Hypotheses :: feats),
     AbsorbSkolemDefs]
    []
-*}
+\<close>
 
 consts SEU882_5_bnd_sK1_Xy :: TPTP_Interpret.ind
 lemma
@@ -437,7 +437,7 @@
 (* apply (erule_tac x = "(@X. False)" in allE) *)
 (* apply (tactic {*remove_redundant_quantification 1*}) *)
 (* apply assumption *)
-by (tactic {*nonfull_extcnf_combined_tac @{context} [RemoveRedundantQuantifications, Extuni_FlexRigid]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [RemoveRedundantQuantifications, Extuni_FlexRigid]\<close>)
 
 (*NUM667^1*)
 (*
@@ -472,7 +472,7 @@
              (\<not> SEU602_2_bnd_in (SEU602_2_bnd_sK7_E SV49) SEU602_2_bnd_sK2_SY17)) =
             False"
 (*FIXME this (and similar) tests are getting the "Bad background theory of goal state" error since upgrading to Isabelle2013-2.*)
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Extuni_Func, Existential_Var]\<close>)
 
 consts
   SEV405_5_bnd_sK1_SY2 :: "(TPTP_Interpret.ind \<Rightarrow> bool) \<Rightarrow> TPTP_Interpret.ind"
@@ -487,7 +487,7 @@
             (\<not> (\<not> (\<not> SV1 (SEV405_5_bnd_sK1_SY2 SV1) \<or> SEV405_5_bnd_cA) \<or>
                 \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) =
             False"
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Existential_Var]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
 (*
 strip quantifiers -- creating a space of permutations; from shallowest to deepest (iterative deepening)
 flip the conclusion -- giving us branch
@@ -503,38 +503,38 @@
 (*testing parameters*)
 lemma "! X :: TPTP_Interpret.ind . (\<forall>A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
 \<Longrightarrow> ! X :: TPTP_Interpret.ind . (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "(A & B) = True ==> (A | B) = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "(\<not> bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True \<Longrightarrow> (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*testing goals with parameters*)
 lemma "(\<not> bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = True \<Longrightarrow> ! X. (bnd_subset (bnd_dsetconstr bnd_sK1 bnd_sK2) bnd_sK1) = False"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "(A & B) = True ==> (B & A) = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*appreciating differences between THEN, REPEAT, and APPEND*)
 lemma "A & B ==> B & A"
-apply (tactic {*
+apply (tactic \<open>
   TRY (etac @{thm conjE} 1)
-  THEN TRY (rtac @{thm conjI} 1)*})
+  THEN TRY (rtac @{thm conjI} 1)\<close>)
 by assumption+
 
 lemma "A & B ==> B & A"
-by (tactic {*
+by (tactic \<open>
   etac @{thm conjE} 1
   THEN rtac @{thm conjI} 1
-  THEN REPEAT (atac 1)*})
+  THEN REPEAT (atac 1)\<close>)
 
 lemma "A & B ==> B & A"
-apply (tactic {*
+apply (tactic \<open>
   rtac @{thm conjI} 1
-  APPEND etac @{thm conjE} 1*})+
+  APPEND etac @{thm conjE} 1\<close>)+
 back
 by assumption+
 
@@ -564,16 +564,16 @@
            \<not> SV1 bnd_c1 bnd_c1) \<or>
           SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2) =
          True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "(\<not> SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = True \<Longrightarrow> (SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1) = False"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*testing repeated application of simulator*)
 lemma "(\<not> \<not> False) = True \<Longrightarrow>
     SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
     False = True \<or> False = True \<or> False = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*Testing non-normal conclusion. Ideally we should be able to apply
   the tactic to arbitrary chains of extcnf steps -- where it's not
@@ -581,48 +581,48 @@
 lemma "(\<not> \<not> False) = True \<Longrightarrow>
     SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
     (\<not> False) = False"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*testing repeated application of simulator, involving different extcnf rules*)
 lemma "(\<not> \<not> (False | False)) = True \<Longrightarrow>
     SEU581_2_bnd_subset (SEU581_2_bnd_dsetconstr SEU581_2_bnd_sK1 SEU581_2_bnd_sK2) SEU581_2_bnd_sK1 = True \<or>
     False = True \<or> False = True \<or> False = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*testing logical expansion*)
 lemma "(\<forall>A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
 \<Longrightarrow> (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*testing extcnf_forall_pos*)
 lemma "(\<forall>A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True \<Longrightarrow> \<forall>SV1. (\<forall>SY14.
              SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14)
               (SEU581_2_bnd_powerset SV1)) = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "((\<forall>A Xphi. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr A Xphi) (SEU581_2_bnd_powerset A)) = True) | ((~ False) = False) \<Longrightarrow>
 \<forall>SV1. ((\<forall>SY14. SEU581_2_bnd_in (SEU581_2_bnd_dsetconstr SV1 SY14) (SEU581_2_bnd_powerset SV1)) = True) | ((~ False) = False)"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*testing parameters*)
 lemma "(\<forall>A B. SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
 \<Longrightarrow> ! X. (\<forall>A B. \<not> SEU581_2_bnd_in B (SEU581_2_bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "((? A .P1 A) = False) | P2 = True \<Longrightarrow> !X. ((P1 X) = False | P2 = True)"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "((!A . (P1a A | P1b A)) = True) | (P2 = True) \<Longrightarrow> !X. (P1a X = True | P1b X = True | P2 = True)"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \<Longrightarrow> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \<Longrightarrow> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "! Y. (((!A .(P1a A | P1b A)) = True) | P2 = True) \<Longrightarrow> ! Y. (!X. (P1a X = True | P1b X = True | P2 = True))"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 consts dud_bnd_s :: "TPTP_Interpret.ind \<Rightarrow> TPTP_Interpret.ind"
 
@@ -636,12 +636,12 @@
           \<not> PUZ114_5_bnd_sK3 SX0 SX1 \<or>
           PUZ114_5_bnd_sK3 (dud_bnd_s SX0) (dud_bnd_s SX1))) =
    False"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*testing logical expansion -- this should be done by blast*)
 lemma "(\<forall>A B. bnd_in B (bnd_powerset A) \<longrightarrow> SEU581_2_bnd_subset B A) = True
 \<Longrightarrow> (\<forall>A B. \<not> bnd_in B (bnd_powerset A) \<or> SEU581_2_bnd_subset B A) = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 (*testing related to PUZ114^5.p.out*)
 lemma "\<forall>SV1. ((\<not> (\<not> SV1 (PUZ114_5_bnd_sK4 SV1) (PUZ114_5_bnd_sK5 SV1) \<or>
@@ -660,7 +660,7 @@
                           (bnd_s (PUZ114_5_bnd_sK5 SV1))))) =
                 True) \<or>
                SV1 PUZ114_5_bnd_sK1 PUZ114_5_bnd_sK2 = True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "\<forall>SV2. (\<forall>SY41.
                    \<not> PUZ114_5_bnd_sK3 SV2 SY41 \<or>
@@ -670,7 +670,7 @@
             (\<not> PUZ114_5_bnd_sK3 SV2 SV4 \<or>
              PUZ114_5_bnd_sK3 (dud_bnd_s (dud_bnd_s SV2)) SV4) =
             True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 lemma "\<forall>SV3. (\<forall>SY42.
                    \<not> PUZ114_5_bnd_sK3 SV3 SY42 \<or>
@@ -680,7 +680,7 @@
             (\<not> PUZ114_5_bnd_sK3 SV3 SV5 \<or>
              PUZ114_5_bnd_sK3 (dud_bnd_s SV3) (dud_bnd_s SV5)) =
             True"
-by (tactic {*full_extcnf_combined_tac @{context}*})
+by (tactic \<open>full_extcnf_combined_tac @{context}\<close>)
 
 
 subsection "unfold_def"
@@ -749,7 +749,7 @@
        (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
          bnd_emptyset))))))) =
                  True"
-by (tactic {*unfold_def_tac @{context} []*})
+by (tactic \<open>unfold_def_tac @{context} []\<close>)
 
      (* (Annotated_step ("10", "unfold_def"), *)
 lemma "bnd_kpairiskpair =
@@ -817,7 +817,7 @@
     (bnd_setadjoin (bnd_setadjoin SX2 (bnd_setadjoin SX3 bnd_emptyset))
       bnd_emptyset)))))) =
                  True"
-by (tactic {*unfold_def_tac @{context} []*})
+by (tactic \<open>unfold_def_tac @{context} []\<close>)
 
      (* (Annotated_step ("12", "unfold_def"), *)
 lemma "bnd_cCKB6_BLACK =
@@ -854,7 +854,7 @@
 apply (tactic {*log_expander 1*})+
 apply (rule refl)
 *)
-by (tactic {*unfold_def_tac @{context} []*})
+by (tactic \<open>unfold_def_tac @{context} []\<close>)
 
      (* (Annotated_step ("13", "unfold_def"), *)
 lemma "bnd_cCKB6_BLACK =
@@ -887,10 +887,10 @@
 apply (tactic {*expander_animal 1*})+
 apply assumption
 *)
-by (tactic {*unfold_def_tac @{context} []*})
+by (tactic \<open>unfold_def_tac @{context} []\<close>)
 
 (*FIXME move this heuristic elsewhere*)
-ML {*
+ML \<open>
 (*Other than the list (which must not be empty) this function
   expects a parameter indicating the smallest integer.
   (Using Int.minInt isn't always viable).*)
@@ -905,13 +905,13 @@
   let
     val max = max_int_floored min l
   in find_index (pair max #> op =) l end
-*}
+\<close>
 
-ML {*
+ML \<open>
 max_index_floored 0 [1, 3, 5]
-*}
+\<close>
 
-ML {*
+ML \<open>
 (*
 Given argument ([h_1, ..., h_n], conc),
 obtained from term of form
@@ -925,9 +925,9 @@
     map size_of_term hypos
     |> max_index_floored 0
     |> SOME
-*}
+\<close>
 
-ML {*
+ML \<open>
 fun biggest_hyp_first_tac i = fn st =>
   let
     val results = TERMFUN biggest_hypothesis (SOME i) st
@@ -944,7 +944,7 @@
               if n > 0 then rotate_tac n i st else no_tac st
       end
   end
-*}
+\<close>
 
      (* (Annotated_step ("6", "unfold_def"), *)
 lemma  "(\<not> (\<exists>U :: TPTP_Interpret.ind \<Rightarrow> bool. \<forall>V. U V = SEV405_5_bnd_cA)) = True \<Longrightarrow>
@@ -1006,7 +1006,7 @@
              GEG007_1_bnd_c (GEG007_1_bnd_sK7_SX2 SV13 SV6) GEG007_1_bnd_catalunya) =
             False \<or>
             GEG007_1_bnd_a SV6 SV13 = False"
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Existential_Var]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
 
      (* (Annotated_step ("116", "extcnf_forall_neg"), *)
 lemma "\<forall>SV13 SV6.
@@ -1039,7 +1039,7 @@
       \<not> (\<forall>SX4. \<not> GEG007_1_bnd_c SX4 SY71 \<or> GEG007_1_bnd_c SX4 GEG007_1_bnd_spain)))))) =
             False \<or>
             GEG007_1_bnd_a SV6 SV13 = False"
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Existential_Var]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
 
 consts PUZ107_5_bnd_sK1_SX0 ::
   "TPTP_Interpret.ind
@@ -1056,7 +1056,7 @@
    (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
    ((SV1 = SV3) = True \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
    PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Not_neg]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Not_neg]\<close>)
 
 lemma "
 \<forall>(SV8::TPTP_Interpret.ind) (SV6::TPTP_Interpret.ind)
@@ -1070,7 +1070,7 @@
    (SV3::TPTP_Interpret.ind) SV1::TPTP_Interpret.ind.
    ((SV1 \<noteq> SV3) = False \<or> PUZ107_5_bnd_sK1_SX0 SV1 SV2 SV6 SV8 = False) \<or>
    PUZ107_5_bnd_sK1_SX0 SV3 SV4 SV6 SV8 = False"
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Or_neg]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Or_neg]\<close>)
 
 consts
   NUM016_5_bnd_a :: TPTP_Interpret.ind
@@ -1149,7 +1149,7 @@
                    NUM016_5_bnd_less (NUM016_5_bnd_factorial_plus_one NUM016_5_bnd_a)
                     SX0))) =
          True"
-by (tactic {*unfold_def_tac @{context} []*})
+by (tactic \<open>unfold_def_tac @{context} []\<close>)
 
      (* (Annotated_step ("3", "unfold_def"), *)
 lemma "(~ ((((((((((((ALL X. ~ bnd_less X X) &
@@ -1189,13 +1189,13 @@
                      (ALL X. (~ bnd_prime X | ~ bnd_less bnd_a X) |
                              bnd_less (bnd_factorial_plus_one bnd_a) X))) =
                  False"
-by (tactic {*unfold_def_tac @{context} []*})
+by (tactic \<open>unfold_def_tac @{context} []\<close>)
 
 (* SET062^6.p.out
       [[(Annotated_step ("3", "unfold_def"), *)
 lemma "(\<forall>Z3. False \<longrightarrow> bnd_cA Z3) = False \<Longrightarrow>
          (\<forall>Z3. False \<longrightarrow> bnd_cA Z3) = False"
-by (tactic {*unfold_def_tac @{context} []*})
+by (tactic \<open>unfold_def_tac @{context} []\<close>)
 
 (*
 (* SEU559^2.p.out *)
@@ -1253,7 +1253,7 @@
          False \<Longrightarrow>
          AGT037_2_bnd_possibly_likes AGT037_2_bnd_jan AGT037_2_bnd_cola AGT037_2_bnd_sK1_SX0 =
          False"
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Existential_Var]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
 
      (* (Annotated_step ("202", "extcnf_forall_neg"), *)
 lemma "\<forall>(SV13::TPTP_Interpret.ind) (SV39::AGT037_2_bnd_mu) (SV29::AGT037_2_bnd_mu)
@@ -1297,7 +1297,7 @@
 apply (tactic {*clause_breaker 1*})
 apply (tactic {*nonfull_extcnf_combined_tac []*})
 *)
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Existential_Var]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
 
 (*(*NUM667^1*)
 lemma "\<forall>SV12 SV13 SV14 SV9 SV10 SV11.
@@ -2157,7 +2157,7 @@
                 \<not> (\<not> SEV405_5_bnd_cA \<or> SV1 (SEV405_5_bnd_sK1_SY2 SV1)))) =
             False"
 (* apply (tactic {*full_extcnf_combined_tac*}) *)
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Existential_Var]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Existential_Var]\<close>)
 
      (* (Annotated_step ("13", "extcnf_forall_pos"), *)
 lemma "(\<forall>SY31 SY32.
@@ -2168,7 +2168,7 @@
                    bnd_sK2 (bnd_sK4 SV1 SY42) =
                    bnd_sK5 (bnd_sK2 SV1) (bnd_sK2 SY42)) =
                True"
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Universal]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Universal]\<close>)
 
      (* (Annotated_step ("14", "extcnf_forall_pos"), *)
 lemma "(\<forall>SY35 SY36.
@@ -2179,7 +2179,7 @@
                    bnd_sK1 (bnd_sK3 SV2 SY43) =
                    bnd_sK4 (bnd_sK1 SV2) (bnd_sK1 SY43)) =
                True"
-by (tactic {*nonfull_extcnf_combined_tac @{context} [Universal]*})
+by (tactic \<open>nonfull_extcnf_combined_tac @{context} [Universal]\<close>)
 
 
 (*from SYO198^5.p.out*)
@@ -2188,7 +2188,7 @@
              \<not> \<not> (\<not> SX0 bnd_sK1_Xx \<or> \<not> SX0 bnd_sK2_Xy)) =
          True \<Longrightarrow>
          (\<not> \<not> (\<not> True \<or> \<not> True)) = True"
-apply (tactic {*extcnf_forall_special_pos_tac 1*})
+apply (tactic \<open>extcnf_forall_special_pos_tac 1\<close>)
 done
 
      (* (Annotated_step ("13", "extcnf_forall_special_pos"), *)
@@ -2196,7 +2196,7 @@
              \<not> \<not> (\<not> SX0 bnd_sK1_Xx \<or> \<not> SX0 bnd_sK2_Xy)) =
          True \<Longrightarrow>
          (\<not> \<not> (\<not> bnd_sK1_Xx \<or> \<not> bnd_sK2_Xy)) = True"
-apply (tactic {*extcnf_forall_special_pos_tac 1*})
+apply (tactic \<open>extcnf_forall_special_pos_tac 1\<close>)
 done
 
    (* [[(Annotated_step ("8", "polarity_switch"), *)
@@ -2205,7 +2205,7 @@
          (\<not> (\<forall>(Xx::bool) (Xy::bool) Xz::bool.
                 True \<and> True \<longrightarrow> True)) =
          True"
-apply (tactic {*nonfull_extcnf_combined_tac @{context} [Polarity_switch]*})
+apply (tactic \<open>nonfull_extcnf_combined_tac @{context} [Polarity_switch]\<close>)
 done
 
 lemma "((\<forall>SY22 SY23 SY24.
@@ -2224,7 +2224,7 @@
           (\<forall>SY28. SY25 SY28 \<longrightarrow> bnd_sK1_RRR SY28 SY27) \<longrightarrow>
           bnd_sK1_RRR (bnd_sK2_U SY25) SY27)) =
   True"
-apply (tactic {*standard_cnf_tac @{context} 1*})
+apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
 done
 
 lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
@@ -2236,7 +2236,7 @@
   False \<Longrightarrow>
  (\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) =
   True"
-apply (tactic {*standard_cnf_tac @{context} 1*})
+apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
 done
 
 lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
@@ -2248,7 +2248,7 @@
   False \<Longrightarrow>
   (\<forall>Xx Xy. bnd_in Xx (bnd_setadjoin Xx Xy)) =
   True"
-apply (tactic {*standard_cnf_tac @{context} 1*})
+apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
 done
 
 lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
@@ -2261,7 +2261,7 @@
   (\<forall>A B. A = B \<longrightarrow>
          (\<forall>Xx Xy. Xx = Xy \<longrightarrow> bnd_in Xx A = bnd_in Xy B)) =
   True"
-apply (tactic {*standard_cnf_tac @{context} 1*})
+apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
 done
 
 lemma "((\<forall>Xx. bnd_in Xx bnd_emptyset \<longrightarrow> (\<forall>Xphi. Xphi)) \<longrightarrow>
@@ -2274,7 +2274,7 @@
   (\<forall>SY0. bnd_in SY0 bnd_omega \<longrightarrow>
          bnd_setadjoin SY0 SY0 \<noteq> bnd_emptyset) =
   False"
-apply (tactic {*standard_cnf_tac @{context} 1*})
+apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
 done
 
 (*nested conjunctions*)
@@ -2287,7 +2287,7 @@
   False \<Longrightarrow>
   (\<forall>Xx. bnd_cP bnd_e Xx = Xx) =
   True"
-apply (tactic {*standard_cnf_tac @{context} 1*})
+apply (tactic \<open>standard_cnf_tac @{context} 1\<close>)
 done
 
 end