diff -r 4939494ed791 -r ce654b0e6d69 src/HOL/TPTP/TPTP_Proof_Reconstruction.thy
--- a/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Tue Feb 13 14:24:50 2018 +0100
+++ b/src/HOL/TPTP/TPTP_Proof_Reconstruction.thy	Thu Feb 15 12:11:00 2018 +0100
@@ -346,8 +346,8 @@
   "(((A :: bool) = B) = True) == (((A \<longrightarrow> B) = True) & ((B \<longrightarrow> A) = True))"
   "((A :: bool) = B) = False == (((~A) | B) = False) | (((~B) | A) = False)"
 
-  "((F = G) = True) == (! x. (F x = G x)) = True"
-  "((F = G) = False) == (! x. (F x = G x)) = False"
+  "((F = G) = True) == (\<forall>x. (F x = G x)) = True"
+  "((F = G) = False) == (\<forall>x. (F x = G x)) = False"
 
   "(A | B) = True == (A = True) | (B = True)"
   "(A & B) = False == (A = False) | (B = False)"
@@ -403,7 +403,7 @@
   "((A \<or> B) = (C \<or> D)) = False \<Longrightarrow> (B = C) = False \<or> (A = D) = False"
 by auto
 
-lemma extuni_func [rule_format]: "(F = G) = False \<Longrightarrow> (! X. (F X = G X)) = False" by auto
+lemma extuni_func [rule_format]: "(F = G) = False \<Longrightarrow> (\<forall>X. (F X = G X)) = False" by auto
 
 
 subsection "Emulation: tactics"
@@ -482,18 +482,18 @@
 subsection "Skolemisation"
 
 lemma skolemise [rule_format]:
-  "\<forall> P. (~ (! x. P x)) \<longrightarrow> ~ (P (SOME x. ~ P x))"
+  "\<forall> P. (\<not> (\<forall>x. P x)) \<longrightarrow> \<not> (P (SOME x. ~ P x))"
 proof -
-  have "\<And> P. (~ (! x. P x)) \<Longrightarrow> ~ (P (SOME x. ~ P x))"
+  have "\<And> P. (\<not> (\<forall>x. P x)) \<Longrightarrow> \<not> (P (SOME x. ~ P x))"
   proof -
     fix P
-    assume ption: "~ (! x. P x)"
-    hence a: "? x. ~ P x" by force
+    assume ption: "\<not> (\<forall>x. P x)"
+    hence a: "\<exists>x. \<not> P x" by force
 
-    have hilbert : "\<And> P. (? x. P x) \<Longrightarrow> (P (SOME x. P x))"
+    have hilbert : "\<And>P. (\<exists>x. P x) \<Longrightarrow> (P (SOME x. P x))"
     proof -
       fix P
-      assume "(? x. P x)"
+      assume "(\<exists>x. P x)"
       thus "(P (SOME x. P x))"
         apply auto
         apply (rule someI)
@@ -501,9 +501,9 @@
         done
     qed
 
-    from a show "~ P (SOME x. ~ P x)"
+    from a show "\<not> P (SOME x. \<not> P x)"
     proof -
-      assume "? x. ~ P x"
+      assume "\<exists>x. \<not> P x"
       hence "\<not> P (SOME x. \<not> P x)" by (rule hilbert)
       thus ?thesis .
     qed
@@ -512,13 +512,13 @@
 qed
 
 lemma polar_skolemise [rule_format]:
-  "\<forall> P. (! x. P x) = False \<longrightarrow> (P (SOME x. ~ P x)) = False"
+  "\<forall>P. (\<forall>x. P x) = False \<longrightarrow> (P (SOME x. \<not> P x)) = False"
 proof -
-  have "\<And> P. (! x. P x) = False \<Longrightarrow> (P (SOME x. ~ P x)) = False"
+  have "\<And>P. (\<forall>x. P x) = False \<Longrightarrow> (P (SOME x. \<not> P x)) = False"
   proof -
     fix P
-    assume ption: "(! x. P x) = False"
-    hence "\<not> (\<forall> x. P x)" by force
+    assume ption: "(\<forall>x. P x) = False"
+    hence "\<not> (\<forall>x. P x)" by force
     hence "\<not> All P" by force
     hence "\<not> (P (SOME x. \<not> P x))" by (rule skolemise)
     thus "(P (SOME x. \<not> P x)) = False" by force
@@ -527,12 +527,12 @@
 qed
 
 lemma leo2_skolemise [rule_format]:
-  "\<forall> P sk. (! x. P x) = False \<longrightarrow> (sk = (SOME x. ~ P x)) \<longrightarrow> (P sk) = False"
+  "\<forall>P sk. (\<forall>x. P x) = False \<longrightarrow> (sk = (SOME x. \<not> P x)) \<longrightarrow> (P sk) = False"
 by (clarify, rule polar_skolemise)
 
 lemma lift_forall [rule_format]:
-  "!! x. (! x. A x) = True ==> (A x) = True"
-  "!! x. (? x. A x) = False ==> (A x) = False"
+  "\<And>x. (\<forall>x. A x) = True \<Longrightarrow> (A x) = True"
+  "\<And>x. (\<exists>x. A x) = False \<Longrightarrow> (A x) = False"
 by auto
 lemma lift_exists [rule_format]:
   "\<lbrakk>(All P) = False; sk = (SOME x. \<not> P x)\<rbrakk> \<Longrightarrow> P sk = False"
@@ -975,7 +975,7 @@
    let
      val simpset =
        empty_simpset ctxt (*NOTE for some reason, Bind exception gets raised if ctxt's simpset isn't emptied*)
-       |> Simplifier.add_simp @{lemma "Ex P == (~ (! x. ~ P x))" by auto}
+       |> Simplifier.add_simp @{lemma "Ex P == (\<not> (\<forall>x. \<not> P x))" by auto}
    in
      CHANGED (asm_full_simp_tac simpset i)
    end
@@ -1541,7 +1541,7 @@
 subsubsection "Finite types"
 (*lift quantification from a singleton literal to a singleton clause*)
 lemma forall_pos_lift:
-"\<lbrakk>(! X. P X) = True; ! X. (P X = True) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by auto
+"\<lbrakk>(\<forall>X. P X) = True; \<forall>X. (P X = True) \<Longrightarrow> R\<rbrakk> \<Longrightarrow> R" by auto
 
 (*predicate over the type of the leading quantified variable*)
 
@@ -1750,10 +1750,10 @@
 \<close>
 
 lemma drop_redundant_literal_qtfr:
-  "(! X. P) = True \<Longrightarrow> P = True"
-  "(? X. P) = True \<Longrightarrow> P = True"
-  "(! X. P) = False \<Longrightarrow> P = False"
-  "(? X. P) = False \<Longrightarrow> P = False"
+  "(\<forall>X. P) = True \<Longrightarrow> P = True"
+  "(\<exists>X. P) = True \<Longrightarrow> P = True"
+  "(\<forall>X. P) = False \<Longrightarrow> P = False"
+  "(\<exists>X. P) = False \<Longrightarrow> P = False"
 by auto
 
 ML \<open>
@@ -1952,11 +1952,11 @@
 subsection "Handling split 'preprocessing'"
 
 lemma split_tranfs:
-  "! x. P x & Q x \<equiv> (! x. P x) & (! x. Q x)"
-  "~ (~ A) \<equiv> A"
-  "? x. A \<equiv> A"
-  "(A & B) & C \<equiv> A & B & C"
-  "A = B \<equiv> (A --> B) & (B --> A)"
+  "\<forall>x. P x \<and> Q x \<equiv> (\<forall>x. P x) \<and> (\<forall>x. Q x)"
+  "\<not> (\<not> A) \<equiv> A"
+  "\<exists>x. A \<equiv> A"
+  "(A \<and> B) \<and> C \<equiv> A \<and> B \<and> C"
+  "A = B \<equiv> (A \<longrightarrow> B) \<and> (B \<longrightarrow> A)"
 by (rule eq_reflection, auto)+
 
 (*Same idiom as ex_expander_tac*)