# HG changeset patch
# User wenzelm
# Date 1445288407 -7200
# Node ID b8d375aee0dfa0ebe3c094c0d3f4965d25dfd154
# Parent  d40cbf1f37c980e0d811565843af1dfa6c8d6705
more symbols;
tunes whitespace;

diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Classical.thy
--- a/src/FOL/ex/Classical.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Classical.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -3,490 +3,526 @@
     Copyright   1994  University of Cambridge
 *)
 
-section\<open>Classical Predicate Calculus Problems\<close>
-
-theory Classical imports FOL begin
-
-lemma "(P --> Q | R) --> (P-->Q) | (P-->R)"
-by blast
+section \<open>Classical Predicate Calculus Problems\<close>
 
-text\<open>If and only if\<close>
+theory Classical
+imports FOL
+begin
 
-lemma "(P<->Q) <-> (Q<->P)"
-by blast
-
-lemma "~ (P <-> ~P)"
-by blast
+lemma "(P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R)"
+  by blast
 
 
-text\<open>Sample problems from 
-  F. J. Pelletier, 
-  Seventy-Five Problems for Testing Automatic Theorem Provers,
-  J. Automated Reasoning 2 (1986), 191-216.
-  Errata, JAR 4 (1988), 236-236.
+subsubsection \<open>If and only if\<close>
+
+lemma "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
+  by blast
+
+lemma "\<not> (P \<longleftrightarrow> \<not> P)"
+  by blast
+
+
+subsection \<open>Pelletier's examples\<close>
 
-The hardest problems -- judging by experience with several theorem provers,
-including matrix ones -- are 34 and 43.
+text \<open>
+  Sample problems from
+
+    \<^item> F. J. Pelletier,
+    Seventy-Five Problems for Testing Automatic Theorem Provers,
+    J. Automated Reasoning 2 (1986), 191-216.
+    Errata, JAR 4 (1988), 236-236.
+
+  The hardest problems -- judging by experience with several theorem
+  provers, including matrix ones -- are 34 and 43.
 \<close>
 
-subsection\<open>Pelletier's examples\<close>
-
 text\<open>1\<close>
-lemma "(P-->Q)  <->  (~Q --> ~P)"
-by blast
+lemma "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
+  by blast
 
 text\<open>2\<close>
-lemma "~ ~ P  <->  P"
-by blast
+lemma "\<not> \<not> P \<longleftrightarrow> P"
+  by blast
 
 text\<open>3\<close>
-lemma "~(P-->Q) --> (Q-->P)"
-by blast
+lemma "\<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
+  by blast
 
 text\<open>4\<close>
-lemma "(~P-->Q)  <->  (~Q --> P)"
-by blast
+lemma "(\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
+  by blast
 
 text\<open>5\<close>
-lemma "((P|Q)-->(P|R)) --> (P|(Q-->R))"
-by blast
+lemma "((P \<or> Q) \<longrightarrow> (P \<or> R)) \<longrightarrow> (P \<or> (Q \<longrightarrow> R))"
+  by blast
 
 text\<open>6\<close>
-lemma "P | ~ P"
-by blast
+lemma "P \<or> \<not> P"
+  by blast
 
 text\<open>7\<close>
-lemma "P | ~ ~ ~ P"
-by blast
+lemma "P \<or> \<not> \<not> \<not> P"
+  by blast
 
-text\<open>8.  Peirce's law\<close>
-lemma "((P-->Q) --> P)  -->  P"
-by blast
+text\<open>8. Peirce's law\<close>
+lemma "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
+  by blast
 
 text\<open>9\<close>
-lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-by blast
+lemma "((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)"
+  by blast
 
 text\<open>10\<close>
-lemma "(Q-->R) & (R-->P&Q) & (P-->Q|R) --> (P<->Q)"
-by blast
+lemma "(Q \<longrightarrow> R) \<and> (R \<longrightarrow> P \<and> Q) \<and> (P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longleftrightarrow> Q)"
+  by blast
 
-text\<open>11.  Proved in each direction (incorrectly, says Pelletier!!)\<close>
-lemma "P<->P"
-by blast
+text\<open>11. Proved in each direction (incorrectly, says Pelletier!!)\<close>
+lemma "P \<longleftrightarrow> P"
+  by blast
 
-text\<open>12.  "Dijkstra's law"\<close>
-lemma "((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
-by blast
+text\<open>12. "Dijkstra's law"\<close>
+lemma "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
+  by blast
 
-text\<open>13.  Distributive law\<close>
-lemma "P | (Q & R)  <-> (P | Q) & (P | R)"
-by blast
+text\<open>13. Distributive law\<close>
+lemma "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+  by blast
 
 text\<open>14\<close>
-lemma "(P <-> Q) <-> ((Q | ~P) & (~Q|P))"
-by blast
+lemma "(P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P))"
+  by blast
 
 text\<open>15\<close>
-lemma "(P --> Q) <-> (~P | Q)"
-by blast
+lemma "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
+  by blast
 
 text\<open>16\<close>
-lemma "(P-->Q) | (Q-->P)"
-by blast
+lemma "(P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"
+  by blast
 
 text\<open>17\<close>
-lemma "((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
-by blast
+lemma "((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S))"
+  by blast
+
 
-subsection\<open>Classical Logic: examples with quantifiers\<close>
+subsection \<open>Classical Logic: examples with quantifiers\<close>
 
-lemma "(\<forall>x. P(x) & Q(x)) <-> (\<forall>x. P(x))  &  (\<forall>x. Q(x))"
-by blast
+lemma "(\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
+  by blast
 
-lemma "(\<exists>x. P-->Q(x))  <->  (P --> (\<exists>x. Q(x)))"
-by blast
+lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
+  by blast
 
-lemma "(\<exists>x. P(x)-->Q)  <->  (\<forall>x. P(x)) --> Q"
-by blast
+lemma "(\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+  by blast
 
-lemma "(\<forall>x. P(x)) | Q  <->  (\<forall>x. P(x) | Q)"
-by blast
+lemma "(\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
+  by blast
 
 text\<open>Discussed in Avron, Gentzen-Type Systems, Resolution and Tableaux,
   JAR 10 (265-281), 1993.  Proof is trivial!\<close>
-lemma "~((\<exists>x.~P(x)) & ((\<exists>x. P(x)) | (\<exists>x. P(x) & Q(x))) & ~ (\<exists>x. P(x)))"
-by blast
+lemma "\<not> ((\<exists>x. \<not> P(x)) \<and> ((\<exists>x. P(x)) \<or> (\<exists>x. P(x) \<and> Q(x))) \<and> \<not> (\<exists>x. P(x)))"
+  by blast
 
-subsection\<open>Problems requiring quantifier duplication\<close>
 
-text\<open>Theorem B of Peter Andrews, Theorem Proving via General Matings, 
+subsection \<open>Problems requiring quantifier duplication\<close>
+
+text\<open>Theorem B of Peter Andrews, Theorem Proving via General Matings,
   JACM 28 (1981).\<close>
-lemma "(\<exists>x. \<forall>y. P(x) <-> P(y)) --> ((\<exists>x. P(x)) <-> (\<forall>y. P(y)))"
-by blast
+lemma "(\<exists>x. \<forall>y. P(x) \<longleftrightarrow> P(y)) \<longrightarrow> ((\<exists>x. P(x)) \<longleftrightarrow> (\<forall>y. P(y)))"
+  by blast
 
 text\<open>Needs multiple instantiation of ALL.\<close>
-lemma "(\<forall>x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
-by blast
+lemma "(\<forall>x. P(x) \<longrightarrow> P(f(x))) \<and> P(d) \<longrightarrow> P(f(f(f(d))))"
+  by blast
 
 text\<open>Needs double instantiation of the quantifier\<close>
-lemma "\<exists>x. P(x) --> P(a) & P(b)"
-by blast
+lemma "\<exists>x. P(x) \<longrightarrow> P(a) \<and> P(b)"
+  by blast
 
-lemma "\<exists>z. P(z) --> (\<forall>x. P(x))"
-by blast
+lemma "\<exists>z. P(z) \<longrightarrow> (\<forall>x. P(x))"
+  by blast
 
-lemma "\<exists>x. (\<exists>y. P(y)) --> P(x)"
-by blast
+lemma "\<exists>x. (\<exists>y. P(y)) \<longrightarrow> P(x)"
+  by blast
 
-text\<open>V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23.  NOT PROVED\<close>
-lemma "\<exists>x x'. \<forall>y. \<exists>z z'.  
-                (~P(y,y) | P(x,x) | ~S(z,x)) &  
-                (S(x,y) | ~S(y,z) | Q(z',z'))  &  
-                (Q(x',y) | ~Q(y,z') | S(x',x'))"
-oops
+text\<open>V. Lifschitz, What Is the Inverse Method?, JAR 5 (1989), 1--23. NOT PROVED.\<close>
+lemma
+  "\<exists>x x'. \<forall>y. \<exists>z z'.
+    (\<not> P(y,y) \<or> P(x,x) \<or> \<not> S(z,x)) \<and>
+    (S(x,y) \<or> \<not> S(y,z) \<or> Q(z',z')) \<and>
+    (Q(x',y) \<or> \<not> Q(y,z') \<or> S(x',x'))"
+  oops
 
 
-
-subsection\<open>Hard examples with quantifiers\<close>
+subsection \<open>Hard examples with quantifiers\<close>
 
 text\<open>18\<close>
-lemma "\<exists>y. \<forall>x. P(y)-->P(x)"
-by blast
+lemma "\<exists>y. \<forall>x. P(y) \<longrightarrow> P(x)"
+  by blast
 
 text\<open>19\<close>
-lemma "\<exists>x. \<forall>y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
-by blast
+lemma "\<exists>x. \<forall>y z. (P(y) \<longrightarrow> Q(z)) \<longrightarrow> (P(x) \<longrightarrow> Q(x))"
+  by blast
 
 text\<open>20\<close>
-lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x)&Q(y)-->R(z)&S(w)))      
-    --> (\<exists>x y. P(x) & Q(y)) --> (\<exists>z. R(z))"
-by blast
+lemma "(\<forall>x y. \<exists>z. \<forall>w. (P(x) \<and> Q(y) \<longrightarrow> R(z) \<and> S(w)))
+  \<longrightarrow> (\<exists>x y. P(x) \<and> Q(y)) \<longrightarrow> (\<exists>z. R(z))"
+  by blast
 
 text\<open>21\<close>
-lemma "(\<exists>x. P-->Q(x)) & (\<exists>x. Q(x)-->P) --> (\<exists>x. P<->Q(x))"
-by blast
+lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> (\<exists>x. P \<longleftrightarrow> Q(x))"
+  by blast
 
 text\<open>22\<close>
-lemma "(\<forall>x. P <-> Q(x))  -->  (P <-> (\<forall>x. Q(x)))"
-by blast
+lemma "(\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
+  by blast
 
 text\<open>23\<close>
-lemma "(\<forall>x. P | Q(x))  <->  (P | (\<forall>x. Q(x)))"
-by blast
+lemma "(\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x)))"
+  by blast
 
 text\<open>24\<close>
-lemma "~(\<exists>x. S(x)&Q(x)) & (\<forall>x. P(x) --> Q(x)|R(x)) &   
-      (~(\<exists>x. P(x)) --> (\<exists>x. Q(x))) & (\<forall>x. Q(x)|R(x) --> S(x))   
-    --> (\<exists>x. P(x)&R(x))"
-by blast
+lemma
+  "\<not> (\<exists>x. S(x) \<and> Q(x)) \<and> (\<forall>x. P(x) \<longrightarrow> Q(x) \<or> R(x)) \<and>
+    (\<not> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))) \<and> (\<forall>x. Q(x) \<or> R(x) \<longrightarrow> S(x))
+    \<longrightarrow> (\<exists>x. P(x) \<and> R(x))"
+  by blast
 
 text\<open>25\<close>
-lemma "(\<exists>x. P(x)) &   
-      (\<forall>x. L(x) --> ~ (M(x) & R(x))) &   
-      (\<forall>x. P(x) --> (M(x) & L(x))) &    
-      ((\<forall>x. P(x)-->Q(x)) | (\<exists>x. P(x)&R(x)))   
-    --> (\<exists>x. Q(x)&P(x))"
-by blast
+lemma
+  "(\<exists>x. P(x)) \<and>
+    (\<forall>x. L(x) \<longrightarrow> \<not> (M(x) \<and> R(x))) \<and>
+    (\<forall>x. P(x) \<longrightarrow> (M(x) \<and> L(x))) \<and>
+    ((\<forall>x. P(x) \<longrightarrow> Q(x)) \<or> (\<exists>x. P(x) \<and> R(x)))
+    \<longrightarrow> (\<exists>x. Q(x) \<and> P(x))"
+  by blast
 
 text\<open>26\<close>
-lemma "((\<exists>x. p(x)) <-> (\<exists>x. q(x))) &  
-      (\<forall>x. \<forall>y. p(x) & q(y) --> (r(x) <-> s(y)))    
-  --> ((\<forall>x. p(x)-->r(x)) <-> (\<forall>x. q(x)-->s(x)))"
-by blast
+lemma
+  "((\<exists>x. p(x)) \<longleftrightarrow> (\<exists>x. q(x))) \<and>
+    (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) \<longleftrightarrow> s(y)))
+  \<longrightarrow> ((\<forall>x. p(x) \<longrightarrow> r(x)) \<longleftrightarrow> (\<forall>x. q(x) \<longrightarrow> s(x)))"
+  by blast
 
 text\<open>27\<close>
-lemma "(\<exists>x. P(x) & ~Q(x)) &    
-      (\<forall>x. P(x) --> R(x)) &    
-      (\<forall>x. M(x) & L(x) --> P(x)) &    
-      ((\<exists>x. R(x) & ~ Q(x)) --> (\<forall>x. L(x) --> ~ R(x)))   
-  --> (\<forall>x. M(x) --> ~L(x))"
-by blast
+lemma
+  "(\<exists>x. P(x) \<and> \<not> Q(x)) \<and>
+    (\<forall>x. P(x) \<longrightarrow> R(x)) \<and>
+    (\<forall>x. M(x) \<and> L(x) \<longrightarrow> P(x)) \<and>
+    ((\<exists>x. R(x) \<and> \<not> Q(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> \<not> R(x)))
+  \<longrightarrow> (\<forall>x. M(x) \<longrightarrow> \<not> L(x))"
+  by blast
 
-text\<open>28.  AMENDED\<close>
-lemma "(\<forall>x. P(x) --> (\<forall>x. Q(x))) &    
-        ((\<forall>x. Q(x)|R(x)) --> (\<exists>x. Q(x)&S(x))) &   
-        ((\<exists>x. S(x)) --> (\<forall>x. L(x) --> M(x)))   
-    --> (\<forall>x. P(x) & L(x) --> M(x))"
-by blast
+text\<open>28. AMENDED\<close>
+lemma
+  "(\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
+    ((\<forall>x. Q(x) \<or> R(x)) \<longrightarrow> (\<exists>x. Q(x) \<and> S(x))) \<and>
+    ((\<exists>x. S(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> M(x)))
+  \<longrightarrow> (\<forall>x. P(x) \<and> L(x) \<longrightarrow> M(x))"
+  by blast
 
-text\<open>29.  Essentially the same as Principia Mathematica *11.71\<close>
-lemma "(\<exists>x. P(x)) & (\<exists>y. Q(y))   
-    --> ((\<forall>x. P(x)-->R(x)) & (\<forall>y. Q(y)-->S(y))   <->      
-         (\<forall>x y. P(x) & Q(y) --> R(x) & S(y)))"
-by blast
+text\<open>29. Essentially the same as Principia Mathematica *11.71\<close>
+lemma
+  "(\<exists>x. P(x)) \<and> (\<exists>y. Q(y))
+    \<longrightarrow> ((\<forall>x. P(x) \<longrightarrow> R(x)) \<and> (\<forall>y. Q(y) \<longrightarrow> S(y)) \<longleftrightarrow>
+      (\<forall>x y. P(x) \<and> Q(y) \<longrightarrow> R(x) \<and> S(y)))"
+  by blast
 
 text\<open>30\<close>
-lemma "(\<forall>x. P(x) | Q(x) --> ~ R(x)) &  
-      (\<forall>x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
-    --> (\<forall>x. S(x))"
-by blast
+lemma
+  "(\<forall>x. P(x) \<or> Q(x) \<longrightarrow> \<not> R(x)) \<and>
+    (\<forall>x. (Q(x) \<longrightarrow> \<not> S(x)) \<longrightarrow> P(x) \<and> R(x))
+    \<longrightarrow> (\<forall>x. S(x))"
+  by blast
 
 text\<open>31\<close>
-lemma "~(\<exists>x. P(x) & (Q(x) | R(x))) &  
-        (\<exists>x. L(x) & P(x)) &  
-        (\<forall>x. ~ R(x) --> M(x))   
-    --> (\<exists>x. L(x) & M(x))"
-by blast
+lemma
+  "\<not> (\<exists>x. P(x) \<and> (Q(x) \<or> R(x))) \<and>
+    (\<exists>x. L(x) \<and> P(x)) \<and>
+    (\<forall>x. \<not> R(x) \<longrightarrow> M(x))
+  \<longrightarrow> (\<exists>x. L(x) \<and> M(x))"
+  by blast
 
 text\<open>32\<close>
-lemma "(\<forall>x. P(x) & (Q(x)|R(x))-->S(x)) &  
-      (\<forall>x. S(x) & R(x) --> L(x)) &  
-      (\<forall>x. M(x) --> R(x))   
-      --> (\<forall>x. P(x) & M(x) --> L(x))"
-by blast
+lemma
+  "(\<forall>x. P(x) \<and> (Q(x) \<or> R(x)) \<longrightarrow> S(x)) \<and>
+    (\<forall>x. S(x) \<and> R(x) \<longrightarrow> L(x)) \<and>
+    (\<forall>x. M(x) \<longrightarrow> R(x))
+  \<longrightarrow> (\<forall>x. P(x) \<and> M(x) \<longrightarrow> L(x))"
+  by blast
 
 text\<open>33\<close>
-lemma "(\<forall>x. P(a) & (P(x)-->P(b))-->P(c))  <->     
-      (\<forall>x. (~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c)))"
-by blast
+lemma
+  "(\<forall>x. P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c)) \<longleftrightarrow>
+    (\<forall>x. (\<not> P(a) \<or> P(x) \<or> P(c)) \<and> (\<not> P(a) \<or> \<not> P(b) \<or> P(c)))"
+  by blast
 
-text\<open>34  AMENDED (TWICE!!).  Andrews's challenge\<close>
-lemma "((\<exists>x. \<forall>y. p(x) <-> p(y))  <->                 
-       ((\<exists>x. q(x)) <-> (\<forall>y. p(y))))     <->         
-      ((\<exists>x. \<forall>y. q(x) <-> q(y))  <->                 
-       ((\<exists>x. p(x)) <-> (\<forall>y. q(y))))"
-by blast
+text\<open>34. AMENDED (TWICE!!). Andrews's challenge.\<close>
+lemma
+  "((\<exists>x. \<forall>y. p(x) \<longleftrightarrow> p(y)) \<longleftrightarrow> ((\<exists>x. q(x)) \<longleftrightarrow> (\<forall>y. p(y)))) \<longleftrightarrow>
+    ((\<exists>x. \<forall>y. q(x) \<longleftrightarrow> q(y)) \<longleftrightarrow> ((\<exists>x. p(x)) \<longleftrightarrow> (\<forall>y. q(y))))"
+  by blast
 
 text\<open>35\<close>
-lemma "\<exists>x y. P(x,y) -->  (\<forall>u v. P(u,v))"
-by blast
+lemma "\<exists>x y. P(x,y) \<longrightarrow> (\<forall>u v. P(u,v))"
+  by blast
 
 text\<open>36\<close>
-lemma "(\<forall>x. \<exists>y. J(x,y)) &  
-      (\<forall>x. \<exists>y. G(x,y)) &  
-      (\<forall>x y. J(x,y) | G(x,y) --> (\<forall>z. J(y,z) | G(y,z) --> H(x,z)))    
-  --> (\<forall>x. \<exists>y. H(x,y))"
-by blast
+lemma
+  "(\<forall>x. \<exists>y. J(x,y)) \<and>
+    (\<forall>x. \<exists>y. G(x,y)) \<and>
+    (\<forall>x y. J(x,y) \<or> G(x,y) \<longrightarrow> (\<forall>z. J(y,z) \<or> G(y,z) \<longrightarrow> H(x,z)))
+  \<longrightarrow> (\<forall>x. \<exists>y. H(x,y))"
+  by blast
 
 text\<open>37\<close>
-lemma "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.  
-           (P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (\<exists>u. Q(u,w)))) &  
-      (\<forall>x z. ~P(x,z) --> (\<exists>y. Q(y,z))) &  
-      ((\<exists>x y. Q(x,y)) --> (\<forall>x. R(x,x)))   
-      --> (\<forall>x. \<exists>y. R(x,y))"
-by blast
+lemma
+  "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
+    (P(x,z) \<longrightarrow> P(y,w)) \<and> P(y,z) \<and> (P(y,w) \<longrightarrow> (\<exists>u. Q(u,w)))) \<and>
+    (\<forall>x z. \<not> P(x,z) \<longrightarrow> (\<exists>y. Q(y,z))) \<and>
+    ((\<exists>x y. Q(x,y)) \<longrightarrow> (\<forall>x. R(x,x)))
+  \<longrightarrow> (\<forall>x. \<exists>y. R(x,y))"
+  by blast
 
 text\<open>38\<close>
-lemma "(\<forall>x. p(a) & (p(x) --> (\<exists>y. p(y) & r(x,y))) -->         
-             (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z)))  <->          
-      (\<forall>x. (~p(a) | p(x) | (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z))) &     
-              (~p(a) | ~(\<exists>y. p(y) & r(x,y)) |                           
-              (\<exists>z. \<exists>w. p(z) & r(x,w) & r(w,z))))"
-by blast
+lemma
+  "(\<forall>x. p(a) \<and> (p(x) \<longrightarrow> (\<exists>y. p(y) \<and> r(x,y))) \<longrightarrow>
+    (\<exists>z. \<exists>w. p(z) \<and> r(x,w) \<and> r(w,z)))  \<longleftrightarrow>
+    (\<forall>x. (\<not> p(a) \<or> p(x) \<or> (\<exists>z. \<exists>w. p(z) \<and> r(x,w) \<and> r(w,z))) \<and>
+      (\<not> p(a) \<or> \<not> (\<exists>y. p(y) \<and> r(x,y)) \<or>
+      (\<exists>z. \<exists>w. p(z) \<and> r(x,w) \<and> r(w,z))))"
+  by blast
 
 text\<open>39\<close>
-lemma "~ (\<exists>x. \<forall>y. F(y,x) <-> ~F(y,y))"
-by blast
+lemma "\<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
+  by blast
 
-text\<open>40.  AMENDED\<close>
-lemma "(\<exists>y. \<forall>x. F(x,y) <-> F(x,x)) -->   
-              ~(\<forall>x. \<exists>y. \<forall>z. F(z,y) <-> ~ F(z,x))"
-by blast
+text\<open>40. AMENDED\<close>
+lemma
+  "(\<exists>y. \<forall>x. F(x,y) \<longleftrightarrow> F(x,x)) \<longrightarrow>
+    \<not> (\<forall>x. \<exists>y. \<forall>z. F(z,y) \<longleftrightarrow> \<not> F(z,x))"
+  by blast
 
 text\<open>41\<close>
-lemma "(\<forall>z. \<exists>y. \<forall>x. f(x,y) <-> f(x,z) & ~ f(x,x))         
-          --> ~ (\<exists>z. \<forall>x. f(x,z))"
-by blast
+lemma
+  "(\<forall>z. \<exists>y. \<forall>x. f(x,y) \<longleftrightarrow> f(x,z) \<and> \<not> f(x,x))
+    \<longrightarrow> \<not> (\<exists>z. \<forall>x. f(x,z))"
+  by blast
 
 text\<open>42\<close>
-lemma "~ (\<exists>y. \<forall>x. p(x,y) <-> ~ (\<exists>z. p(x,z) & p(z,x)))"
-by blast
+lemma "\<not> (\<exists>y. \<forall>x. p(x,y) \<longleftrightarrow> \<not> (\<exists>z. p(x,z) \<and> p(z,x)))"
+  by blast
 
 text\<open>43\<close>
-lemma "(\<forall>x. \<forall>y. q(x,y) <-> (\<forall>z. p(z,x) <-> p(z,y)))      
-          --> (\<forall>x. \<forall>y. q(x,y) <-> q(y,x))"
-by blast
+lemma
+  "(\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> (\<forall>z. p(z,x) \<longleftrightarrow> p(z,y)))
+    \<longrightarrow> (\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> q(y,x))"
+  by blast
 
-(*Other proofs: Can use auto, which cheats by using rewriting!  
+text \<open>
+  Other proofs: Can use @{text auto}, which cheats by using rewriting!
   Deepen_tac alone requires 253 secs.  Or
-  by (mini_tac @{context} 1 THEN Deepen_tac 5 1) *)
+  by (mini_tac 1 THEN Deepen_tac 5 1)
+\<close>
 
 text\<open>44\<close>
-lemma "(\<forall>x. f(x) --> (\<exists>y. g(y) & h(x,y) & (\<exists>y. g(y) & ~ h(x,y)))) &  
-      (\<exists>x. j(x) & (\<forall>y. g(y) --> h(x,y)))                    
-      --> (\<exists>x. j(x) & ~f(x))"
-by blast
+lemma
+  "(\<forall>x. f(x) \<longrightarrow> (\<exists>y. g(y) \<and> h(x,y) \<and> (\<exists>y. g(y) \<and> \<not> h(x,y)))) \<and>
+    (\<exists>x. j(x) \<and> (\<forall>y. g(y) \<longrightarrow> h(x,y)))
+  \<longrightarrow> (\<exists>x. j(x) \<and> \<not> f(x))"
+  by blast
 
 text\<open>45\<close>
-lemma "(\<forall>x. f(x) & (\<forall>y. g(y) & h(x,y) --> j(x,y))   
-                      --> (\<forall>y. g(y) & h(x,y) --> k(y))) &     
-      ~ (\<exists>y. l(y) & k(y)) &                                    
-      (\<exists>x. f(x) & (\<forall>y. h(x,y) --> l(y))                     
-                  & (\<forall>y. g(y) & h(x,y) --> j(x,y)))           
-      --> (\<exists>x. f(x) & ~ (\<exists>y. g(y) & h(x,y)))"
-by blast
+lemma
+  "(\<forall>x. f(x) \<and> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> j(x,y))
+      \<longrightarrow> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> k(y))) \<and>
+      \<not> (\<exists>y. l(y) \<and> k(y)) \<and>
+      (\<exists>x. f(x) \<and> (\<forall>y. h(x,y) \<longrightarrow> l(y)) \<and> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> j(x,y)))
+      \<longrightarrow> (\<exists>x. f(x) \<and> \<not> (\<exists>y. g(y) \<and> h(x,y)))"
+  by blast
 
 
 text\<open>46\<close>
-lemma "(\<forall>x. f(x) & (\<forall>y. f(y) & h(y,x) --> g(y)) --> g(x)) &       
-      ((\<exists>x. f(x) & ~g(x)) -->                                     
-       (\<exists>x. f(x) & ~g(x) & (\<forall>y. f(y) & ~g(y) --> j(x,y)))) &     
-      (\<forall>x y. f(x) & f(y) & h(x,y) --> ~j(y,x))                     
-       --> (\<forall>x. f(x) --> g(x))"
-by blast
+lemma
+  "(\<forall>x. f(x) \<and> (\<forall>y. f(y) \<and> h(y,x) \<longrightarrow> g(y)) \<longrightarrow> g(x)) \<and>
+      ((\<exists>x. f(x) \<and> \<not> g(x)) \<longrightarrow>
+       (\<exists>x. f(x) \<and> \<not> g(x) \<and> (\<forall>y. f(y) \<and> \<not> g(y) \<longrightarrow> j(x,y)))) \<and>
+      (\<forall>x y. f(x) \<and> f(y) \<and> h(x,y) \<longrightarrow> \<not> j(y,x))
+      \<longrightarrow> (\<forall>x. f(x) \<longrightarrow> g(x))"
+  by blast
 
 
-subsection\<open>Problems (mainly) involving equality or functions\<close>
+subsection \<open>Problems (mainly) involving equality or functions\<close>
 
 text\<open>48\<close>
-lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
-by blast
+lemma "(a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c"
+  by blast
 
-text\<open>49  NOT PROVED AUTOMATICALLY.  Hard because it involves substitution
-  for Vars
-  the type constraint ensures that x,y,z have the same type as a,b,u.\<close>
-lemma "(\<exists>x y::'a. \<forall>z. z=x | z=y) & P(a) & P(b) & a~=b  
-                --> (\<forall>u::'a. P(u))"
-apply safe
-apply (rule_tac x = a in allE, assumption)
-apply (rule_tac x = b in allE, assumption, fast)
-       --\<open>blast's treatment of equality can't do it\<close>
-done
+text\<open>49. NOT PROVED AUTOMATICALLY. Hard because it involves substitution for
+  Vars; the type constraint ensures that x,y,z have the same type as a,b,u.\<close>
+lemma
+  "(\<exists>x y::'a. \<forall>z. z = x \<or> z = y) \<and> P(a) \<and> P(b) \<and> a \<noteq> b \<longrightarrow> (\<forall>u::'a. P(u))"
+  apply safe
+  apply (rule_tac x = a in allE, assumption)
+  apply (rule_tac x = b in allE, assumption)
+  apply fast  -- \<open>blast's treatment of equality can't do it\<close>
+  done
 
-text\<open>50.  (What has this to do with equality?)\<close>
-lemma "(\<forall>x. P(a,x) | (\<forall>y. P(x,y))) --> (\<exists>x. \<forall>y. P(x,y))"
-by blast
+text\<open>50. (What has this to do with equality?)\<close>
+lemma "(\<forall>x. P(a,x) \<or> (\<forall>y. P(x,y))) \<longrightarrow> (\<exists>x. \<forall>y. P(x,y))"
+  by blast
 
 text\<open>51\<close>
-lemma "(\<exists>z w. \<forall>x y. P(x,y) <->  (x=z & y=w)) -->   
-      (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) <-> y=w) <-> x=z)"
-by blast
+lemma
+  "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+    (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) \<longleftrightarrow> y=w) \<longleftrightarrow> x = z)"
+  by blast
 
 text\<open>52\<close>
 text\<open>Almost the same as 51.\<close>
-lemma "(\<exists>z w. \<forall>x y. P(x,y) <->  (x=z & y=w)) -->   
-      (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) <-> x=z) <-> y=w)"
-by blast
+lemma
+  "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+    (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) \<longleftrightarrow> x = z) \<longleftrightarrow> y = w)"
+  by blast
 
 text\<open>55\<close>
-
 text\<open>Non-equational version, from Manthey and Bry, CADE-9 (Springer, 1988).
   fast DISCOVERS who killed Agatha.\<close>
-schematic_goal "lives(agatha) & lives(butler) & lives(charles) &  
-   (killed(agatha,agatha) | killed(butler,agatha) | killed(charles,agatha)) &  
-   (\<forall>x y. killed(x,y) --> hates(x,y) & ~richer(x,y)) &  
-   (\<forall>x. hates(agatha,x) --> ~hates(charles,x)) &  
-   (hates(agatha,agatha) & hates(agatha,charles)) &  
-   (\<forall>x. lives(x) & ~richer(x,agatha) --> hates(butler,x)) &  
-   (\<forall>x. hates(agatha,x) --> hates(butler,x)) &  
-   (\<forall>x. ~hates(x,agatha) | ~hates(x,butler) | ~hates(x,charles)) -->  
+schematic_goal
+  "lives(agatha) \<and> lives(butler) \<and> lives(charles) \<and>
+   (killed(agatha,agatha) \<or> killed(butler,agatha) \<or> killed(charles,agatha)) \<and>
+   (\<forall>x y. killed(x,y) \<longrightarrow> hates(x,y) \<and> \<not> richer(x,y)) \<and>
+   (\<forall>x. hates(agatha,x) \<longrightarrow> \<not> hates(charles,x)) \<and>
+   (hates(agatha,agatha) \<and> hates(agatha,charles)) \<and>
+   (\<forall>x. lives(x) \<and> \<not> richer(x,agatha) \<longrightarrow> hates(butler,x)) \<and>
+   (\<forall>x. hates(agatha,x) \<longrightarrow> hates(butler,x)) \<and>
+   (\<forall>x. \<not> hates(x,agatha) \<or> \<not> hates(x,butler) \<or> \<not> hates(x,charles)) \<longrightarrow>
     killed(?who,agatha)"
-by fast --\<open>MUCH faster than blast\<close>
+  by fast  -- \<open>MUCH faster than blast\<close>
 
 
 text\<open>56\<close>
-lemma "(\<forall>x. (\<exists>y. P(y) & x=f(y)) --> P(x)) <-> (\<forall>x. P(x) --> P(f(x)))"
-by blast
+lemma "(\<forall>x. (\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
+  by blast
 
 text\<open>57\<close>
-lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &  
-     (\<forall>x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
-by blast
+lemma
+  "P(f(a,b), f(b,c)) \<and> P(f(b,c), f(a,c)) \<and>
+    (\<forall>x y z. P(x,y) \<and> P(y,z) \<longrightarrow> P(x,z)) \<longrightarrow> P(f(a,b), f(a,c))"
+  by blast
 
 text\<open>58  NOT PROVED AUTOMATICALLY\<close>
-lemma "(\<forall>x y. f(x)=g(y)) --> (\<forall>x y. f(f(x))=f(g(y)))"
-by (slow elim: subst_context)
+lemma "(\<forall>x y. f(x) = g(y)) \<longrightarrow> (\<forall>x y. f(f(x)) = f(g(y)))"
+  by (slow elim: subst_context)
 
 
 text\<open>59\<close>
-lemma "(\<forall>x. P(x) <-> ~P(f(x))) --> (\<exists>x. P(x) & ~P(f(x)))"
-by blast
+lemma "(\<forall>x. P(x) \<longleftrightarrow> \<not> P(f(x))) \<longrightarrow> (\<exists>x. P(x) \<and> \<not> P(f(x)))"
+  by blast
 
 text\<open>60\<close>
-lemma "\<forall>x. P(x,f(x)) <-> (\<exists>y. (\<forall>z. P(z,y) --> P(z,f(x))) & P(x,y))"
-by blast
+lemma "\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
+  by blast
 
 text\<open>62 as corrected in JAR 18 (1997), page 135\<close>
-lemma "(\<forall>x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->      
-      (\<forall>x. (~p(a) | p(x) | p(f(f(x)))) &                       
-              (~p(a) | ~p(f(x)) | p(f(f(x)))))"
-by blast
+lemma
+  "(\<forall>x. p(a) \<and> (p(x) \<longrightarrow> p(f(x))) \<longrightarrow> p(f(f(x)))) \<longleftrightarrow>
+    (\<forall>x. (\<not> p(a) \<or> p(x) \<or> p(f(f(x)))) \<and>
+      (\<not> p(a) \<or> \<not> p(f(x)) \<or> p(f(f(x)))))"
+  by blast
 
-text\<open>From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
+text \<open>From Davis, Obvious Logical Inferences, IJCAI-81, 530-531
   fast indeed copes!\<close>
-lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &  
-              (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y))) &    
-              (\<forall>x. K(x) --> ~G(x))  -->  (\<exists>x. K(x) & J(x))"
-by fast
+lemma
+  "(\<forall>x. F(x) \<and> \<not> G(x) \<longrightarrow> (\<exists>y. H(x,y) \<and> J(y))) \<and>
+    (\<exists>x. K(x) \<and> F(x) \<and> (\<forall>y. H(x,y) \<longrightarrow> K(y))) \<and>
+    (\<forall>x. K(x) \<longrightarrow> \<not> G(x)) \<longrightarrow> (\<exists>x. K(x) \<and> J(x))"
+  by fast
 
-text\<open>From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.  
+text \<open>From Rudnicki, Obvious Inferences, JAR 3 (1987), 383-393.
   It does seem obvious!\<close>
-lemma "(\<forall>x. F(x) & ~G(x) --> (\<exists>y. H(x,y) & J(y))) &         
-      (\<exists>x. K(x) & F(x) & (\<forall>y. H(x,y) --> K(y)))  &         
-      (\<forall>x. K(x) --> ~G(x))   -->   (\<exists>x. K(x) --> ~G(x))"
-by fast
+lemma
+  "(\<forall>x. F(x) \<and> \<not> G(x) \<longrightarrow> (\<exists>y. H(x,y) \<and> J(y))) \<and>
+    (\<exists>x. K(x) \<and> F(x) \<and> (\<forall>y. H(x,y) \<longrightarrow> K(y))) \<and>
+    (\<forall>x. K(x) \<longrightarrow> \<not> G(x)) \<longrightarrow> (\<exists>x. K(x) \<longrightarrow> \<not> G(x))"
+  by fast
 
-text\<open>Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
-  author U. Egly\<close>
-lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->                
-   (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z)))))                   
-  &                                                                      
-  (\<forall>w. C(w) & (\<forall>u. C(u) --> (\<forall>v. D(w,u,v))) -->                 
-        (\<forall>y z.                                                        
-            (C(y) &  P(y,z) --> Q(w,y,z) & OO(w,g)) &                    
-            (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))                    
-  &                                                                      
-  (\<forall>w. C(w) &                                                         
-    (\<forall>y z.                                                            
-        (C(y) & P(y,z) --> Q(w,y,z) & OO(w,g)) &                         
-        (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))) -->                     
-    (\<exists>v. C(v) &                                                        
-          (\<forall>y. ((C(y) & Q(w,y,y)) & OO(w,g) --> ~P(v,y)) &            
-                  ((C(y) & Q(w,y,y)) & OO(w,b) --> P(v,y) & OO(v,b)))))  
-   -->                   
-   ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
-by (blast 12)
-   --\<open>Needed because the search for depths below 12 is very slow\<close>
+text \<open>Halting problem: Formulation of Li Dafa (AAR Newsletter 27, Oct 1994.)
+  author U. Egly.\<close>
+lemma
+  "((\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z)))) \<longrightarrow>
+     (\<exists>w. C(w) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(w,y,z)))))
+    \<and>
+    (\<forall>w. C(w) \<and> (\<forall>u. C(u) \<longrightarrow> (\<forall>v. D(w,u,v))) \<longrightarrow>
+          (\<forall>y z.
+              (C(y) \<and> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,g)) \<and>
+              (C(y) \<and> \<not> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,b))))
+    \<and>
+    (\<forall>w. C(w) \<and>
+      (\<forall>y z.
+          (C(y) \<and> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,g)) \<and>
+          (C(y) \<and> \<not> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,b))) \<longrightarrow>
+      (\<exists>v. C(v) \<and>
+            (\<forall>y. ((C(y) \<and> Q(w,y,y)) \<and> OO(w,g) \<longrightarrow> \<not> P(v,y)) \<and>
+                    ((C(y) \<and> Q(w,y,y)) \<and> OO(w,b) \<longrightarrow> P(v,y) \<and> OO(v,b)))))
+     \<longrightarrow> \<not> (\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z))))"
+  by (blast 12)
+    -- \<open>Needed because the search for depths below 12 is very slow.\<close>
 
 
-text\<open>Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1), p.105\<close>
-lemma "((\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z)))) -->        
-   (\<exists>w. C(w) & (\<forall>y. C(y) --> (\<forall>z. D(w,y,z)))))           
-  &                                                              
-  (\<forall>w. C(w) & (\<forall>u. C(u) --> (\<forall>v. D(w,u,v))) -->         
-        (\<forall>y z.                                                
-            (C(y) &  P(y,z) --> Q(w,y,z) & OO(w,g)) &           
-            (C(y) & ~P(y,z) --> Q(w,y,z) & OO(w,b))))          
-  &                                                              
-  ((\<exists>w. C(w) & (\<forall>y. (C(y) &  P(y,y) --> Q(w,y,y) & OO(w,g)) & 
-                         (C(y) & ~P(y,y) --> Q(w,y,y) & OO(w,b))))  
-   -->                                                             
-   (\<exists>v. C(v) & (\<forall>y. (C(y) &  P(y,y) --> P(v,y) & OO(v,g)) &   
-                         (C(y) & ~P(y,y) --> P(v,y) & OO(v,b)))))  
-  -->                                                              
-  ((\<exists>v. C(v) & (\<forall>y. (C(y) &  P(y,y) --> P(v,y) & OO(v,g)) &   
-                         (C(y) & ~P(y,y) --> P(v,y) & OO(v,b))))   
-   -->                                                             
-   (\<exists>u. C(u) & (\<forall>y. (C(y) &  P(y,y) --> ~P(u,y)) &     
-                         (C(y) & ~P(y,y) --> P(u,y) & OO(u,b)))))  
-   -->                                                             
-   ~ (\<exists>x. A(x) & (\<forall>y. C(y) --> (\<forall>z. D(x,y,z))))"
-by blast
+text \<open>
+  Halting problem II: credited to M. Bruschi by Li Dafa in JAR 18(1),
+  p. 105.
+\<close>
+lemma
+  "((\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z)))) \<longrightarrow>
+     (\<exists>w. C(w) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(w,y,z)))))
+    \<and>
+    (\<forall>w. C(w) \<and> (\<forall>u. C(u) \<longrightarrow> (\<forall>v. D(w,u,v))) \<longrightarrow>
+          (\<forall>y z.
+              (C(y) \<and> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,g)) \<and>
+              (C(y) \<and> \<not> P(y,z) \<longrightarrow> Q(w,y,z) \<and> OO(w,b))))
+    \<and>
+    ((\<exists>w. C(w) \<and> (\<forall>y. (C(y) \<and> P(y,y) \<longrightarrow> Q(w,y,y) \<and> OO(w,g)) \<and>
+                           (C(y) \<and> \<not> P(y,y) \<longrightarrow> Q(w,y,y) \<and> OO(w,b))))
+     \<longrightarrow>
+     (\<exists>v. C(v) \<and> (\<forall>y. (C(y) \<and> P(y,y) \<longrightarrow> P(v,y) \<and> OO(v,g)) \<and>
+                           (C(y) \<and> \<not> P(y,y) \<longrightarrow> P(v,y) \<and> OO(v,b)))))
+    \<longrightarrow>
+    ((\<exists>v. C(v) \<and> (\<forall>y. (C(y) \<and> P(y,y) \<longrightarrow> P(v,y) \<and> OO(v,g)) \<and>
+                           (C(y) \<and> \<not> P(y,y) \<longrightarrow> P(v,y) \<and> OO(v,b))))
+     \<longrightarrow>
+     (\<exists>u. C(u) \<and> (\<forall>y. (C(y) \<and> P(y,y) \<longrightarrow> \<not> P(u,y)) \<and>
+                           (C(y) \<and> \<not> P(y,y) \<longrightarrow> P(u,y) \<and> OO(u,b)))))
+     \<longrightarrow> \<not> (\<exists>x. A(x) \<and> (\<forall>y. C(y) \<longrightarrow> (\<forall>z. D(x,y,z))))"
+  by blast
 
-text\<open>Challenge found on info-hol\<close>
-lemma "\<forall>x. \<exists>v w. \<forall>y z. P(x) & Q(y) --> (P(v) | R(w)) & (R(z) --> Q(v))"
-by blast
+text \<open>Challenge found on info-hol.\<close>
+lemma "\<forall>x. \<exists>v w. \<forall>y z. P(x) \<and> Q(y) \<longrightarrow> (P(v) \<or> R(w)) \<and> (R(z) \<longrightarrow> Q(v))"
+  by blast
 
-text\<open>Attributed to Lewis Carroll by S. G. Pulman.  The first or last assumption
-can be deleted.\<close>
-lemma "(\<forall>x. honest(x) & industrious(x) --> healthy(x)) &  
-      ~ (\<exists>x. grocer(x) & healthy(x)) &  
-      (\<forall>x. industrious(x) & grocer(x) --> honest(x)) &  
-      (\<forall>x. cyclist(x) --> industrious(x)) &  
-      (\<forall>x. ~healthy(x) & cyclist(x) --> ~honest(x))   
-      --> (\<forall>x. grocer(x) --> ~cyclist(x))"
-by blast
+text \<open>
+  Attributed to Lewis Carroll by S. G. Pulman. The first or last assumption
+  can be deleted.\<close>
+lemma
+  "(\<forall>x. honest(x) \<and> industrious(x) \<longrightarrow> healthy(x)) \<and>
+    \<not> (\<exists>x. grocer(x) \<and> healthy(x)) \<and>
+    (\<forall>x. industrious(x) \<and> grocer(x) \<longrightarrow> honest(x)) \<and>
+    (\<forall>x. cyclist(x) \<longrightarrow> industrious(x)) \<and>
+    (\<forall>x. \<not> healthy(x) \<and> cyclist(x) \<longrightarrow> \<not> honest(x))
+    \<longrightarrow> (\<forall>x. grocer(x) \<longrightarrow> \<not> cyclist(x))"
+  by blast
 
 
 (*Runtimes for old versions of this file:
-Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2] 
-Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac] 
-Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip] 
-Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions] 
+Thu Jul 23 1992: loaded in 467s using iffE [on SPARC2]
+Mon Nov 14 1994: loaded in 144s [on SPARC10, with deepen_tac]
+Wed Nov 16 1994: loaded in 138s [after addition of norm_term_skip]
+Mon Nov 21 1994: loaded in 131s [DEPTH_FIRST suppressing repetitions]
 
 Further runtimes on a Sun-4
-Tue Mar  4 1997: loaded in 93s (version 94-7) 
+Tue Mar  4 1997: loaded in 93s (version 94-7)
 Tue Mar  4 1997: loaded in 89s
 Thu Apr  3 1997: loaded in 44s--using mostly Blast_tac
 Thu Apr  3 1997: loaded in 96s--addition of two Halting Probs
@@ -497,4 +533,3 @@
 *)
 
 end
-
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Foundation.thy
--- a/src/FOL/ex/Foundation.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Foundation.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -9,7 +9,7 @@
 imports IFOL
 begin
 
-lemma "A&B  --> (C-->A&C)"
+lemma "A \<and> B \<longrightarrow> (C \<longrightarrow> A \<and> C)"
 apply (rule impI)
 apply (rule impI)
 apply (rule conjI)
@@ -20,8 +20,8 @@
 
 text \<open>A form of conj-elimination\<close>
 lemma
-  assumes "A & B"
-    and "A ==> B ==> C"
+  assumes "A \<and> B"
+    and "A \<Longrightarrow> B \<Longrightarrow> C"
   shows C
 apply (rule assms)
 apply (rule conjunct1)
@@ -31,26 +31,26 @@
 done
 
 lemma
-  assumes "!!A. ~ ~A ==> A"
-  shows "B | ~B"
+  assumes "\<And>A. \<not> \<not> A \<Longrightarrow> A"
+  shows "B \<or> \<not> B"
 apply (rule assms)
 apply (rule notI)
-apply (rule_tac P = "~B" in notE)
+apply (rule_tac P = "\<not> B" in notE)
 apply (rule_tac [2] notI)
-apply (rule_tac [2] P = "B | ~B" in notE)
+apply (rule_tac [2] P = "B \<or> \<not> B" in notE)
 prefer 2 apply assumption
 apply (rule_tac [2] disjI1)
 prefer 2 apply assumption
 apply (rule notI)
-apply (rule_tac P = "B | ~B" in notE)
+apply (rule_tac P = "B \<or> \<not> B" in notE)
 apply assumption
 apply (rule disjI2)
 apply assumption
 done
 
 lemma
-  assumes "!!A. ~ ~A ==> A"
-  shows "B | ~B"
+  assumes "\<And>A. \<not> \<not> A \<Longrightarrow> A"
+  shows "B \<or> \<not> B"
 apply (rule assms)
 apply (rule notI)
 apply (rule notE)
@@ -64,14 +64,14 @@
 
 
 lemma
-  assumes "A | ~A"
-    and "~ ~A"
+  assumes "A \<or> \<not> A"
+    and "\<not> \<not> A"
   shows A
 apply (rule disjE)
 apply (rule assms)
 apply assumption
 apply (rule FalseE)
-apply (rule_tac P = "~A" in notE)
+apply (rule_tac P = "\<not> A" in notE)
 apply (rule assms)
 apply assumption
 done
@@ -80,27 +80,27 @@
 subsection "Examples with quantifiers"
 
 lemma
-  assumes "ALL z. G(z)"
-  shows "ALL z. G(z)|H(z)"
+  assumes "\<forall>z. G(z)"
+  shows "\<forall>z. G(z) \<or> H(z)"
 apply (rule allI)
 apply (rule disjI1)
 apply (rule assms [THEN spec])
 done
 
-lemma "ALL x. EX y. x=y"
+lemma "\<forall>x. \<exists>y. x = y"
 apply (rule allI)
 apply (rule exI)
 apply (rule refl)
 done
 
-lemma "EX y. ALL x. x=y"
+lemma "\<exists>y. \<forall>x. x = y"
 apply (rule exI)
 apply (rule allI)
 apply (rule refl)?
 oops
 
 text \<open>Parallel lifting example.\<close>
-lemma "EX u. ALL x. EX v. ALL y. EX w. P(u,x,v,y,w)"
+lemma "\<exists>u. \<forall>x. \<exists>v. \<forall>y. \<exists>w. P(u,x,v,y,w)"
 apply (rule exI allI)
 apply (rule exI allI)
 apply (rule exI allI)
@@ -109,8 +109,8 @@
 oops
 
 lemma
-  assumes "(EX z. F(z)) & B"
-  shows "EX z. F(z) & B"
+  assumes "(\<exists>z. F(z)) \<and> B"
+  shows "\<exists>z. F(z) \<and> B"
 apply (rule conjE)
 apply (rule assms)
 apply (rule exE)
@@ -122,7 +122,7 @@
 done
 
 text \<open>A bigger demonstration of quantifiers -- not in the paper.\<close>
-lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
+lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
 apply (rule impI)
 apply (rule allI)
 apply (rule exE, assumption)
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/If.thy
--- a/src/FOL/ex/If.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/If.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -5,57 +5,56 @@
 
 section \<open>First-Order Logic: the 'if' example\<close>
 
-theory If imports FOL begin
-
-definition "if" :: "[o,o,o]=>o" where
-  "if(P,Q,R) == P&Q | ~P&R"
+theory If
+imports FOL
+begin
 
-lemma ifI:
-    "[| P ==> Q; ~P ==> R |] ==> if(P,Q,R)"
-apply (simp add: if_def, blast)
-done
+definition "if" :: "[o,o,o]=>o"
+  where "if(P,Q,R) \<equiv> P \<and> Q \<or> \<not> P \<and> R"
+
+lemma ifI: "\<lbrakk>P \<Longrightarrow> Q; \<not> P \<Longrightarrow> R\<rbrakk> \<Longrightarrow> if(P,Q,R)"
+  unfolding if_def by blast
 
-lemma ifE:
-   "[| if(P,Q,R);  [| P; Q |] ==> S; [| ~P; R |] ==> S |] ==> S"
-apply (simp add: if_def, blast)
-done
+lemma ifE: "\<lbrakk>if(P,Q,R); \<lbrakk>P; Q\<rbrakk> \<Longrightarrow> S; \<lbrakk>\<not> P; R\<rbrakk> \<Longrightarrow> S\<rbrakk> \<Longrightarrow> S"
+  unfolding if_def by blast
 
-lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
-apply (rule iffI)
-apply (erule ifE)
-apply (erule ifE)
-apply (rule ifI)
-apply (rule ifI)
-oops
+lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) \<longleftrightarrow> if(Q, if(P,A,C), if(P,B,D))"
+  apply (rule iffI)
+  apply (erule ifE)
+  apply (erule ifE)
+  apply (rule ifI)
+  apply (rule ifI)
+  oops
 
 text\<open>Trying again from the beginning in order to use @{text blast}\<close>
 declare ifI [intro!]
 declare ifE [elim!]
 
-lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) <-> if(Q, if(P,A,C), if(P,B,D))"
-by blast
+lemma if_commute: "if(P, if(Q,A,B), if(Q,C,D)) \<longleftrightarrow> if(Q, if(P,A,C), if(P,B,D))"
+  by blast
 
 
-lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
-by blast
+lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,A,B))"
+  by blast
 
 text\<open>Trying again from the beginning in order to prove from the definitions\<close>
-lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,A,B))"
-by (simp add: if_def, blast)
+lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,A,B))"
+  unfolding if_def by blast
 
 
-text\<open>An invalid formula.  High-level rules permit a simpler diagnosis\<close>
-lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
-apply auto
-  -- \<open>The next step will fail unless subgoals remain\<close>
-apply (tactic all_tac)
-oops
+text \<open>An invalid formula. High-level rules permit a simpler diagnosis.\<close>
+lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))"
+  apply auto
+    -- \<open>The next step will fail unless subgoals remain\<close>
+  apply (tactic all_tac)
+  oops
 
-text\<open>Trying again from the beginning in order to prove from the definitions\<close>
-lemma "if(if(P,Q,R), A, B) <-> if(P, if(Q,A,B), if(R,B,A))"
-apply (simp add: if_def, auto) 
-  -- \<open>The next step will fail unless subgoals remain\<close>
-apply (tactic all_tac)
-oops
+text \<open>Trying again from the beginning in order to prove from the definitions.\<close>
+lemma "if(if(P,Q,R), A, B) \<longleftrightarrow> if(P, if(Q,A,B), if(R,B,A))"
+  unfolding if_def
+  apply auto
+    -- \<open>The next step will fail unless subgoals remain\<close>
+  apply (tactic all_tac)
+  oops
 
 end
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Intro.thy
--- a/src/FOL/ex/Intro.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Intro.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -13,7 +13,7 @@
 
 subsubsection \<open>Some simple backward proofs\<close>
 
-lemma mythm: "P|P --> P"
+lemma mythm: "P \<or> P \<longrightarrow> P"
 apply (rule impI)
 apply (rule disjE)
 prefer 3 apply (assumption)
@@ -21,7 +21,7 @@
 apply assumption
 done
 
-lemma "(P & Q) | R --> (P | R)"
+lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R)"
 apply (rule impI)
 apply (erule disjE)
 apply (drule conjunct1)
@@ -30,8 +30,8 @@
 apply assumption+
 done
 
-(*Correct version, delaying use of "spec" until last*)
-lemma "(ALL x y. P(x,y)) --> (ALL z w. P(w,z))"
+text \<open>Correct version, delaying use of @{text spec} until last.\<close>
+lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>z w. P(w,z))"
 apply (rule impI)
 apply (rule allI)
 apply (rule allI)
@@ -43,14 +43,12 @@
 
 subsubsection \<open>Demonstration of @{text "fast"}\<close>
 
-lemma "(EX y. ALL x. J(y,x) <-> ~J(x,x))
-        -->  ~ (ALL x. EX y. ALL z. J(z,y) <-> ~ J(z,x))"
+lemma "(\<exists>y. \<forall>x. J(y,x) \<longleftrightarrow> \<not> J(x,x)) \<longrightarrow> \<not> (\<forall>x. \<exists>y. \<forall>z. J(z,y) \<longleftrightarrow> \<not> J(z,x))"
 apply fast
 done
 
 
-lemma "ALL x. P(x,f(x)) <->
-        (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
+lemma "\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
 apply fast
 done
 
@@ -58,8 +56,8 @@
 subsubsection \<open>Derivation of conjunction elimination rule\<close>
 
 lemma
-  assumes major: "P&Q"
-    and minor: "[| P; Q |] ==> R"
+  assumes major: "P \<and> Q"
+    and minor: "\<lbrakk>P; Q\<rbrakk> \<Longrightarrow> R"
   shows R
 apply (rule minor)
 apply (rule major [THEN conjunct1])
@@ -72,8 +70,8 @@
 text \<open>Derivation of negation introduction\<close>
 
 lemma
-  assumes "P ==> False"
-  shows "~ P"
+  assumes "P \<Longrightarrow> False"
+  shows "\<not> P"
 apply (unfold not_def)
 apply (rule impI)
 apply (rule assms)
@@ -81,7 +79,7 @@
 done
 
 lemma
-  assumes major: "~P"
+  assumes major: "\<not> P"
     and minor: P
   shows R
 apply (rule FalseE)
@@ -92,7 +90,7 @@
 
 text \<open>Alternative proof of the result above\<close>
 lemma
-  assumes major: "~P"
+  assumes major: "\<not> P"
     and minor: P
   shows R
 apply (rule minor [THEN major [unfolded not_def, THEN mp, THEN FalseE]])
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Intuitionistic.thy
--- a/src/FOL/ex/Intuitionistic.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Intuitionistic.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -36,390 +36,417 @@
 intuitionistically provable.  Finally, if $P$ is a negation then $\neg\neg P$
 is intuitionstically equivalent to $P$.  [Andy Pitts]\<close>
 
-lemma "~~(P&Q) <-> ~~P & ~~Q"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> (P \<and> Q) \<longleftrightarrow> \<not> \<not> P \<and> \<not> \<not> Q"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-lemma "~~ ((~P --> Q) --> (~P --> ~Q) --> P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longrightarrow> (\<not> P \<longrightarrow> \<not> Q) \<longrightarrow> P)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>Double-negation does NOT distribute over disjunction\<close>
+text \<open>Double-negation does NOT distribute over disjunction.\<close>
 
-lemma "~~(P-->Q)  <-> (~~P --> ~~Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> \<not> P \<longrightarrow> \<not> \<not> Q)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-lemma "~~~P <-> ~P"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> \<not> P \<longleftrightarrow> \<not> P"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-lemma "~~((P --> Q | R)  -->  (P-->Q) | (P-->R))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> ((P \<longrightarrow> Q \<or> R) \<longrightarrow> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-lemma "(P<->Q) <-> (Q<->P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-lemma "((P --> (Q | (Q-->R))) --> R) --> R"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "((P \<longrightarrow> (Q \<or> (Q \<longrightarrow> R))) \<longrightarrow> R) \<longrightarrow> R"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-lemma "(((G-->A) --> J) --> D --> E) --> (((H-->B)-->I)-->C-->J)
-      --> (A-->H) --> F --> G --> (((C-->B)-->I)-->D)-->(A-->C)
-      --> (((F-->A)-->B) --> I) --> E"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "(((G \<longrightarrow> A) \<longrightarrow> J) \<longrightarrow> D \<longrightarrow> E) \<longrightarrow> (((H \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> C \<longrightarrow> J)
+    \<longrightarrow> (A \<longrightarrow> H) \<longrightarrow> F \<longrightarrow> G \<longrightarrow> (((C \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> D) \<longrightarrow> (A \<longrightarrow> C)
+    \<longrightarrow> (((F \<longrightarrow> A) \<longrightarrow> B) \<longrightarrow> I) \<longrightarrow> E"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 
-text\<open>Lemmas for the propositional double-negation translation\<close>
+subsection \<open>Lemmas for the propositional double-negation translation\<close>
 
-lemma "P --> ~~P"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "P \<longrightarrow> \<not> \<not> P"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-lemma "~~(~~P --> P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> (\<not> \<not> P \<longrightarrow> P)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-lemma "~~P & ~~(P --> Q) --> ~~Q"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> \<not> P \<and> \<not> \<not> (P \<longrightarrow> Q) \<longrightarrow> \<not> \<not> Q"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 
-text\<open>The following are classically but not constructively valid.
-      The attempt to prove them terminates quickly!\<close>
-lemma "((P-->Q) --> P)  -->  P"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
+text \<open>The following are classically but not constructively valid.
+  The attempt to prove them terminates quickly!\<close>
+lemma "((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
+apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
 apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
 oops
 
-lemma "(P&Q-->R)  -->  (P-->R) | (Q-->R)"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
+lemma "(P \<and> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> R) \<or> (Q \<longrightarrow> R)"
+apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
 apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
 oops
 
 
-subsection\<open>de Bruijn formulae\<close>
+subsection \<open>de Bruijn formulae\<close>
 
-text\<open>de Bruijn formula with three predicates\<close>
-lemma "((P<->Q) --> P&Q&R) &
-               ((Q<->R) --> P&Q&R) &
-               ((R<->P) --> P&Q&R) --> P&Q&R"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text \<open>de Bruijn formula with three predicates\<close>
+lemma
+  "((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R) \<and>
+    ((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R) \<and>
+    ((R \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R) \<longrightarrow> P \<and> Q \<and> R"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 
-text\<open>de Bruijn formula with five predicates\<close>
-lemma "((P<->Q) --> P&Q&R&S&T) &
-               ((Q<->R) --> P&Q&R&S&T) &
-               ((R<->S) --> P&Q&R&S&T) &
-               ((S<->T) --> P&Q&R&S&T) &
-               ((T<->P) --> P&Q&R&S&T) --> P&Q&R&S&T"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text \<open>de Bruijn formula with five predicates\<close>
+lemma
+  "((P \<longleftrightarrow> Q) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
+    ((Q \<longleftrightarrow> R) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
+    ((R \<longleftrightarrow> S) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
+    ((S \<longleftrightarrow> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<and>
+    ((T \<longleftrightarrow> P) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T) \<longrightarrow> P \<and> Q \<and> R \<and> S \<and> T"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 
-(*** Problems from of Sahlin, Franzen and Haridi,
-     An Intuitionistic Predicate Logic Theorem Prover.
-     J. Logic and Comp. 2 (5), October 1992, 619-656.
-***)
+text \<open>
+  Problems from of Sahlin, Franzen and Haridi,
+  An Intuitionistic Predicate Logic Theorem Prover.
+  J. Logic and Comp. 2 (5), October 1992, 619-656.
+\<close>
 
 text\<open>Problem 1.1\<close>
-lemma "(ALL x. EX y. ALL z. p(x) & q(y) & r(z)) <->
-      (ALL z. EX y. ALL x. p(x) & q(y) & r(z))"
-by (tactic\<open>IntPr.best_dup_tac @{context} 1\<close>)  --\<open>SLOW\<close>
+lemma
+  "(\<forall>x. \<exists>y. \<forall>z. p(x) \<and> q(y) \<and> r(z)) \<longleftrightarrow>
+    (\<forall>z. \<exists>y. \<forall>x. p(x) \<and> q(y) \<and> r(z))"
+  by (tactic \<open>IntPr.best_dup_tac @{context} 1\<close>)  --\<open>SLOW\<close>
 
 text\<open>Problem 3.1\<close>
-lemma "~ (EX x. ALL y. mem(y,x) <-> ~ mem(x,x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> (\<exists>x. \<forall>y. mem(y,x) \<longleftrightarrow> \<not> mem(x,x))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>Problem 4.1: hopeless!\<close>
-lemma "(ALL x. p(x) --> p(h(x)) | p(g(x))) & (EX x. p(x)) & (ALL x. ~p(h(x)))
-      --> (EX x. p(g(g(g(g(g(x)))))))"
-oops
+lemma
+  "(\<forall>x. p(x) \<longrightarrow> p(h(x)) \<or> p(g(x))) \<and> (\<exists>x. p(x)) \<and> (\<forall>x. \<not> p(h(x)))
+    \<longrightarrow> (\<exists>x. p(g(g(g(g(g(x)))))))"
+  oops
 
 
-subsection\<open>Intuitionistic FOL: propositional problems based on Pelletier.\<close>
+subsection \<open>Intuitionistic FOL: propositional problems based on Pelletier.\<close>
 
-text\<open>~~1\<close>
-lemma "~~((P-->Q)  <->  (~Q --> ~P))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>1\<close>
+lemma "\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~2\<close>
-lemma "~~(~~P  <->  P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>2\<close>
+lemma "\<not> \<not> (\<not> \<not> P \<longleftrightarrow> P)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>3\<close>
-lemma "~(P-->Q) --> (Q-->P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~4\<close>
-lemma "~~((~P-->Q)  <->  (~Q --> P))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>4\<close>
+lemma "\<not> \<not> ((\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~5\<close>
-lemma "~~((P|Q-->P|R) --> P|(Q-->R))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>5\<close>
+lemma "\<not>\<not>((P \<or> Q \<longrightarrow> P \<or> R) \<longrightarrow> P \<or> (Q \<longrightarrow> R))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~6\<close>
-lemma "~~(P | ~P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>6\<close>
+lemma "\<not> \<not> (P \<or> \<not> P)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~7\<close>
-lemma "~~(P | ~~~P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>7\<close>
+lemma "\<not> \<not> (P \<or> \<not> \<not> \<not> P)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~8.  Peirce's law\<close>
-lemma "~~(((P-->Q) --> P)  -->  P)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>8. Peirce's law\<close>
+lemma "\<not> \<not> (((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>9\<close>
-lemma "((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>10\<close>
-lemma "(Q-->R) --> (R-->P&Q) --> (P-->(Q|R)) --> (P<->Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-subsection\<open>11.  Proved in each direction (incorrectly, says Pelletier!!)\<close>
-lemma "P<->P"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~12.  Dijkstra's law\<close>
-lemma "~~(((P <-> Q) <-> R)  <->  (P <-> (Q <-> R)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-lemma "((P <-> Q) <-> R)  -->  ~~(P <-> (Q <-> R))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>13.  Distributive law\<close>
-lemma "P | (Q & R)  <-> (P | Q) & (P | R)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~14\<close>
-lemma "~~((P <-> Q) <-> ((Q | ~P) & (~Q|P)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~15\<close>
-lemma "~~((P --> Q) <-> (~P | Q))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~16\<close>
-lemma "~~((P-->Q) | (Q-->P))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>~~17\<close>
-lemma "~~(((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-text\<open>Dijkstra's "Golden Rule"\<close>
-lemma "(P&Q) <-> P <-> Q <-> (P|Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(Q \<longrightarrow> R) \<longrightarrow> (R \<longrightarrow> P \<and> Q) \<longrightarrow> (P \<longrightarrow> (Q \<or> R)) \<longrightarrow> (P \<longleftrightarrow> Q)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 
-subsection\<open>****Examples with quantifiers****\<close>
+subsection\<open>11. Proved in each direction (incorrectly, says Pelletier!!)\<close>
+
+lemma "P \<longleftrightarrow> P"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>12. Dijkstra's law\<close>
+lemma "\<not> \<not> (((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R)))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longrightarrow> \<not> \<not> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>13. Distributive law\<close>
+lemma "P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>14\<close>
+lemma "\<not> \<not> ((P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P)))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>15\<close>
+lemma "\<not> \<not> ((P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>16\<close>
+lemma "\<not> \<not> ((P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text\<open>\<not>\<not>17\<close>
+lemma "\<not> \<not> (((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S)))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+text \<open>Dijkstra's ``Golden Rule''\<close>
+lemma "(P \<and> Q) \<longleftrightarrow> P \<longleftrightarrow> Q \<longleftrightarrow> (P \<or> Q)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+
+section \<open>Examples with quantifiers\<close>
+
+subsection \<open>The converse is classical in the following implications \dots\<close>
+
+lemma "(\<exists>x. P(x) \<longrightarrow> Q) \<longrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "((\<forall>x. P(x)) \<longrightarrow> Q) \<longrightarrow> \<not> (\<forall>x. P(x) \<and> \<not> Q)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "((\<forall>x. \<not> P(x)) \<longrightarrow> Q) \<longrightarrow> \<not> (\<forall>x. \<not> (P(x) \<or> Q))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "(\<forall>x. P(x)) \<or> Q \<longrightarrow> (\<forall>x. P(x) \<or> Q)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+
+lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<longrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 
-subsection\<open>The converse is classical in the following implications...\<close>
+subsection \<open>The following are not constructively valid!\<close>
+text \<open>The attempt to prove them terminates quickly!\<close>
 
-lemma "(EX x. P(x)-->Q)  -->  (ALL x. P(x)) --> Q"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "((\<forall>x. P(x)) \<longrightarrow> Q) \<longrightarrow> (\<exists>x. P(x) \<longrightarrow> Q)"
+  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  oops
 
-lemma "((ALL x. P(x))-->Q) --> ~ (ALL x. P(x) & ~Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<longrightarrow> (\<exists>x. P \<longrightarrow> Q(x))"
+  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  oops
 
-lemma "((ALL x. ~P(x))-->Q)  -->  ~ (ALL x. ~ (P(x)|Q))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(\<forall>x. P(x) \<or> Q) \<longrightarrow> ((\<forall>x. P(x)) \<or> Q)"
+  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  oops
 
-lemma "(ALL x. P(x)) | Q  -->  (ALL x. P(x) | Q)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(\<forall>x. \<not> \<not> P(x)) \<longrightarrow> \<not> \<not> (\<forall>x. P(x))"
+  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  oops
 
-lemma "(EX x. P --> Q(x)) --> (P --> (EX x. Q(x)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-
-
+text \<open>Classically but not intuitionistically valid.  Proved by a bug in 1986!\<close>
+lemma "\<exists>x. Q(x) \<longrightarrow> (\<forall>x. Q(x))"
+  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)?
+  apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
+  oops
 
 
-subsection\<open>The following are not constructively valid!\<close>
-text\<open>The attempt to prove them terminates quickly!\<close>
-
-lemma "((ALL x. P(x))-->Q) --> (EX x. P(x)-->Q)"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
+subsection \<open>Hard examples with quantifiers\<close>
 
-lemma "(P --> (EX x. Q(x))) --> (EX x. P-->Q(x))"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
-
-lemma "(ALL x. P(x) | Q) --> ((ALL x. P(x)) | Q)"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
+text \<open>
+  The ones that have not been proved are not known to be valid! Some will
+  require quantifier duplication -- not currently available.
+\<close>
 
-lemma "(ALL x. ~~P(x)) --> ~~(ALL x. P(x))"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
-
-text\<open>Classically but not intuitionistically valid.  Proved by a bug in 1986!\<close>
-lemma "EX x. Q(x) --> (ALL x. Q(x))"
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close> | -)
-apply (rule asm_rl) --\<open>Checks that subgoals remain: proof failed.\<close>
-oops
-
+text\<open>\<not>\<not>18\<close>
+lemma "\<not> \<not> (\<exists>y. \<forall>x. P(y) \<longrightarrow> P(x))"
+  oops  -- \<open>NOT PROVED\<close>
 
-subsection\<open>Hard examples with quantifiers\<close>
-
-text\<open>The ones that have not been proved are not known to be valid!
-  Some will require quantifier duplication -- not currently available\<close>
-
-text\<open>~~18\<close>
-lemma "~~(EX y. ALL x. P(y)-->P(x))"
-oops  --\<open>NOT PROVED\<close>
-
-text\<open>~~19\<close>
-lemma "~~(EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x)))"
-oops  --\<open>NOT PROVED\<close>
+text\<open>\<not>\<not>19\<close>
+lemma "\<not> \<not> (\<exists>x. \<forall>y z. (P(y) \<longrightarrow> Q(z)) \<longrightarrow> (P(x) \<longrightarrow> Q(x)))"
+  oops  -- \<open>NOT PROVED\<close>
 
 text\<open>20\<close>
-lemma "(ALL x y. EX z. ALL w. (P(x)&Q(y)-->R(z)&S(w)))
-    --> (EX x y. P(x) & Q(y)) --> (EX z. R(z))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "(\<forall>x y. \<exists>z. \<forall>w. (P(x) \<and> Q(y) \<longrightarrow> R(z) \<and> S(w)))
+    \<longrightarrow> (\<exists>x y. P(x) \<and> Q(y)) \<longrightarrow> (\<exists>z. R(z))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>21\<close>
-lemma "(EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> ~~(EX x. P<->Q(x))"
-oops --\<open>NOT PROVED; needs quantifier duplication\<close>
+lemma "(\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> \<not> \<not> (\<exists>x. P \<longleftrightarrow> Q(x))"
+  oops -- \<open>NOT PROVED; needs quantifier duplication\<close>
 
 text\<open>22\<close>
-lemma "(ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~23\<close>
-lemma "~~ ((ALL x. P | Q(x))  <->  (P | (ALL x. Q(x))))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>23\<close>
+lemma "\<not> \<not> ((\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x))))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>24\<close>
-lemma "~(EX x. S(x)&Q(x)) & (ALL x. P(x) --> Q(x)|R(x)) &
-     (~(EX x. P(x)) --> (EX x. Q(x))) & (ALL x. Q(x)|R(x) --> S(x))
-    --> ~~(EX x. P(x)&R(x))"
-txt\<open>Not clear why @{text fast_tac}, @{text best_tac}, @{text ASTAR} and 
-    @{text ITER_DEEPEN} all take forever\<close>
-apply (tactic\<open>IntPr.safe_tac @{context}\<close>)
-apply (erule impE)
-apply (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "\<not> (\<exists>x. S(x) \<and> Q(x)) \<and> (\<forall>x. P(x) \<longrightarrow> Q(x) \<or> R(x)) \<and>
+    (\<not> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))) \<and> (\<forall>x. Q(x) \<or> R(x) \<longrightarrow> S(x))
+    \<longrightarrow> \<not> \<not> (\<exists>x. P(x) \<and> R(x))"
+text \<open>
+  Not clear why @{text fast_tac}, @{text best_tac}, @{text ASTAR} and
+  @{text ITER_DEEPEN} all take forever.
+\<close>
+  apply (tactic \<open>IntPr.safe_tac @{context}\<close>)
+  apply (erule impE)
+  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+  apply (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
+  done
 
 text\<open>25\<close>
-lemma "(EX x. P(x)) &
-        (ALL x. L(x) --> ~ (M(x) & R(x))) &
-        (ALL x. P(x) --> (M(x) & L(x))) &
-        ((ALL x. P(x)-->Q(x)) | (EX x. P(x)&R(x)))
-    --> (EX x. Q(x)&P(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "(\<exists>x. P(x)) \<and>
+      (\<forall>x. L(x) \<longrightarrow> \<not> (M(x) \<and> R(x))) \<and>
+      (\<forall>x. P(x) \<longrightarrow> (M(x) \<and> L(x))) \<and>
+      ((\<forall>x. P(x) \<longrightarrow> Q(x)) \<or> (\<exists>x. P(x) \<and> R(x)))
+    \<longrightarrow> (\<exists>x. Q(x) \<and> P(x))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~26\<close>
-lemma "(~~(EX x. p(x)) <-> ~~(EX x. q(x))) &
-      (ALL x. ALL y. p(x) & q(y) --> (r(x) <-> s(y)))
-  --> ((ALL x. p(x)-->r(x)) <-> (ALL x. q(x)-->s(x)))"
-oops  --\<open>NOT PROVED\<close>
+text\<open>\<not>\<not>26\<close>
+lemma
+  "(\<not> \<not> (\<exists>x. p(x)) \<longleftrightarrow> \<not> \<not> (\<exists>x. q(x))) \<and>
+    (\<forall>x. \<forall>y. p(x) \<and> q(y) \<longrightarrow> (r(x) \<longleftrightarrow> s(y)))
+  \<longrightarrow> ((\<forall>x. p(x) \<longrightarrow> r(x)) \<longleftrightarrow> (\<forall>x. q(x) \<longrightarrow> s(x)))"
+  oops  --\<open>NOT PROVED\<close>
 
 text\<open>27\<close>
-lemma "(EX x. P(x) & ~Q(x)) &
-              (ALL x. P(x) --> R(x)) &
-              (ALL x. M(x) & L(x) --> P(x)) &
-              ((EX x. R(x) & ~ Q(x)) --> (ALL x. L(x) --> ~ R(x)))
-          --> (ALL x. M(x) --> ~L(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "(\<exists>x. P(x) \<and> \<not> Q(x)) \<and>
+    (\<forall>x. P(x) \<longrightarrow> R(x)) \<and>
+    (\<forall>x. M(x) \<and> L(x) \<longrightarrow> P(x)) \<and>
+    ((\<exists>x. R(x) \<and> \<not> Q(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> \<not> R(x)))
+  \<longrightarrow> (\<forall>x. M(x) \<longrightarrow> \<not> L(x))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~28.  AMENDED\<close>
-lemma "(ALL x. P(x) --> (ALL x. Q(x))) &
-        (~~(ALL x. Q(x)|R(x)) --> (EX x. Q(x)&S(x))) &
-        (~~(EX x. S(x)) --> (ALL x. L(x) --> M(x)))
-    --> (ALL x. P(x) & L(x) --> M(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>28. AMENDED\<close>
+lemma
+  "(\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
+      (\<not> \<not> (\<forall>x. Q(x) \<or> R(x)) \<longrightarrow> (\<exists>x. Q(x) \<and> S(x))) \<and>
+      (\<not> \<not> (\<exists>x. S(x)) \<longrightarrow> (\<forall>x. L(x) \<longrightarrow> M(x)))
+    \<longrightarrow> (\<forall>x. P(x) \<and> L(x) \<longrightarrow> M(x))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>29.  Essentially the same as Principia Mathematica *11.71\<close>
-lemma "(EX x. P(x)) & (EX y. Q(y))
-    --> ((ALL x. P(x)-->R(x)) & (ALL y. Q(y)-->S(y))   <->
-         (ALL x y. P(x) & Q(y) --> R(x) & S(y)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>29. Essentially the same as Principia Mathematica *11.71\<close>
+lemma
+  "(\<exists>x. P(x)) \<and> (\<exists>y. Q(y))
+    \<longrightarrow> ((\<forall>x. P(x) \<longrightarrow> R(x)) \<and> (\<forall>y. Q(y) \<longrightarrow> S(y)) \<longleftrightarrow>
+      (\<forall>x y. P(x) \<and> Q(y) \<longrightarrow> R(x) \<and> S(y)))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~30\<close>
-lemma "(ALL x. (P(x) | Q(x)) --> ~ R(x)) &
-        (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))
-    --> (ALL x. ~~S(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>\<not>\<not>30\<close>
+lemma
+  "(\<forall>x. (P(x) \<or> Q(x)) \<longrightarrow> \<not> R(x)) \<and>
+      (\<forall>x. (Q(x) \<longrightarrow> \<not> S(x)) \<longrightarrow> P(x) \<and> R(x))
+    \<longrightarrow> (\<forall>x. \<not> \<not> S(x))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>31\<close>
-lemma "~(EX x. P(x) & (Q(x) | R(x))) &
-        (EX x. L(x) & P(x)) &
-        (ALL x. ~ R(x) --> M(x))
-    --> (EX x. L(x) & M(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "\<not> (\<exists>x. P(x) \<and> (Q(x) \<or> R(x))) \<and>
+      (\<exists>x. L(x) \<and> P(x)) \<and>
+      (\<forall>x. \<not> R(x) \<longrightarrow> M(x))
+  \<longrightarrow> (\<exists>x. L(x) \<and> M(x))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>32\<close>
-lemma "(ALL x. P(x) & (Q(x)|R(x))-->S(x)) &
-        (ALL x. S(x) & R(x) --> L(x)) &
-        (ALL x. M(x) --> R(x))
-    --> (ALL x. P(x) & M(x) --> L(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "(\<forall>x. P(x) \<and> (Q(x) \<or> R(x)) \<longrightarrow> S(x)) \<and>
+    (\<forall>x. S(x) \<and> R(x) \<longrightarrow> L(x)) \<and>
+    (\<forall>x. M(x) \<longrightarrow> R(x))
+  \<longrightarrow> (\<forall>x. P(x) \<and> M(x) \<longrightarrow> L(x))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>~~33\<close>
-lemma "(ALL x. ~~(P(a) & (P(x)-->P(b))-->P(c)))  <->
-      (ALL x. ~~((~P(a) | P(x) | P(c)) & (~P(a) | ~P(b) | P(c))))"
-apply (tactic\<open>IntPr.best_tac @{context} 1\<close>)
-done
+text\<open>\<not>\<not>33\<close>
+lemma
+  "(\<forall>x. \<not> \<not> (P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c))) \<longleftrightarrow>
+    (\<forall>x. \<not> \<not> ((\<not> P(a) \<or> P(x) \<or> P(c)) \<and> (\<not> P(a) \<or> \<not> P(b) \<or> P(c))))"
+  apply (tactic \<open>IntPr.best_tac @{context} 1\<close>)
+  done
 
 
 text\<open>36\<close>
-lemma "(ALL x. EX y. J(x,y)) &
-      (ALL x. EX y. G(x,y)) &
-      (ALL x y. J(x,y) | G(x,y) --> (ALL z. J(y,z) | G(y,z) --> H(x,z)))
-  --> (ALL x. EX y. H(x,y))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "(\<forall>x. \<exists>y. J(x,y)) \<and>
+    (\<forall>x. \<exists>y. G(x,y)) \<and>
+    (\<forall>x y. J(x,y) \<or> G(x,y) \<longrightarrow> (\<forall>z. J(y,z) \<or> G(y,z) \<longrightarrow> H(x,z)))
+  \<longrightarrow> (\<forall>x. \<exists>y. H(x,y))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>37\<close>
-lemma "(ALL z. EX w. ALL x. EX y.
-           ~~(P(x,z)-->P(y,w)) & P(y,z) & (P(y,w) --> (EX u. Q(u,w)))) &
-        (ALL x z. ~P(x,z) --> (EX y. Q(y,z))) &
-        (~~(EX x y. Q(x,y)) --> (ALL x. R(x,x)))
-    --> ~~(ALL x. EX y. R(x,y))"
-oops  --\<open>NOT PROVED\<close>
+lemma
+  "(\<forall>z. \<exists>w. \<forall>x. \<exists>y.
+      \<not> \<not> (P(x,z) \<longrightarrow> P(y,w)) \<and> P(y,z) \<and> (P(y,w) \<longrightarrow> (\<exists>u. Q(u,w)))) \<and>
+        (\<forall>x z. \<not> P(x,z) \<longrightarrow> (\<exists>y. Q(y,z))) \<and>
+        (\<not> \<not> (\<exists>x y. Q(x,y)) \<longrightarrow> (\<forall>x. R(x,x)))
+    \<longrightarrow> \<not> \<not> (\<forall>x. \<exists>y. R(x,y))"
+  oops  --\<open>NOT PROVED\<close>
 
 text\<open>39\<close>
-lemma "~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
-text\<open>40.  AMENDED\<close>
-lemma "(EX y. ALL x. F(x,y) <-> F(x,x)) -->
-              ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text\<open>40. AMENDED\<close>
+lemma
+  "(\<exists>y. \<forall>x. F(x,y) \<longleftrightarrow> F(x,x)) \<longrightarrow>
+    \<not> (\<forall>x. \<exists>y. \<forall>z. F(z,y) \<longleftrightarrow> \<not> F(z,x))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>44\<close>
-lemma "(ALL x. f(x) -->
-              (EX y. g(y) & h(x,y) & (EX y. g(y) & ~ h(x,y))))  &
-              (EX x. j(x) & (ALL y. g(y) --> h(x,y)))
-              --> (EX x. j(x) & ~f(x))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "(\<forall>x. f(x) \<longrightarrow>
+    (\<exists>y. g(y) \<and> h(x,y) \<and> (\<exists>y. g(y) \<and> \<not> h(x,y)))) \<and>
+    (\<exists>x. j(x) \<and> (\<forall>y. g(y) \<longrightarrow> h(x,y)))
+    \<longrightarrow> (\<exists>x. j(x) \<and> \<not> f(x))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>48\<close>
-lemma "(a=b | c=d) & (a=c | b=d) --> a=d | b=c"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>51\<close>
-lemma "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->
-     (EX z. ALL x. EX w. (ALL y. P(x,y) <-> y=w) <-> x=z)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+    (\<exists>z. \<forall>x. \<exists>w. (\<forall>y. P(x,y) \<longleftrightarrow> y = w) \<longleftrightarrow> x = z)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>52\<close>
-text\<open>Almost the same as 51.\<close>
-lemma "(EX z w. ALL x y. P(x,y) <->  (x=z & y=w)) -->
-     (EX w. ALL y. EX z. (ALL x. P(x,y) <-> x=z) <-> y=w)"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+text \<open>Almost the same as 51.\<close>
+lemma
+  "(\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+    (\<exists>w. \<forall>y. \<exists>z. (\<forall>x. P(x,y) \<longleftrightarrow> x = z) \<longleftrightarrow> y = w)"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>56\<close>
-lemma "(ALL x. (EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "(\<forall>x. (\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>57\<close>
-lemma "P(f(a,b), f(b,c)) & P(f(b,c), f(a,c)) &
-     (ALL x y z. P(x,y) & P(y,z) --> P(x,z))    -->   P(f(a,b), f(a,c))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma
+  "P(f(a,b), f(b,c)) \<and> P(f(b,c), f(a,c)) \<and>
+    (\<forall>x y z. P(x,y) \<and> P(y,z) \<longrightarrow> P(x,z)) \<longrightarrow> P(f(a,b), f(a,c))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 text\<open>60\<close>
-lemma "ALL x. P(x,f(x)) <-> (EX y. (ALL z. P(z,y) --> P(z,f(x))) & P(x,y))"
-by (tactic\<open>IntPr.fast_tac @{context} 1\<close>)
+lemma "\<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
+  by (tactic \<open>IntPr.fast_tac @{context} 1\<close>)
 
 end
-
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Locale_Test/Locale_Test.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -16,9 +16,9 @@
 lemmas less_mixin_thy_merge2 = le'.less_def
 end
 
-lemma "gless(x, y) <-> gle(x, y) & x ~= y" (* mixin from first interpretation applied *)
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" (* mixin from first interpretation applied *)
   by (rule le1.less_mixin_thy_merge1)
-lemma "gless'(x, y) <-> gle'(x, y) & x ~= y" (* mixin from second interpretation applied *)
+lemma "gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y" (* mixin from second interpretation applied *)
   by (rule le1.less_mixin_thy_merge2)
 
 end
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Locale_Test/Locale_Test1.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test1.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -114,8 +114,8 @@
     and P :: "'a => 'b => o"
 begin
 
-definition test :: "'a => o" where
-  "test(x) <-> (ALL b. P(x, b))"
+definition test :: "'a => o"
+  where "test(x) \<longleftrightarrow> (\<forall>b. P(x, b))"
 
 end
 
@@ -133,8 +133,8 @@
     and p2 :: "'b => o"
 begin
 
-definition d1 :: "'a => o" where "d1(x) <-> ~ p2(p1(x))"
-definition d2 :: "'b => o" where "d2(x) <-> ~ p2(x)"
+definition d1 :: "'a => o" where "d1(x) \<longleftrightarrow> \<not> p2(p1(x))"
+definition d2 :: "'b => o" where "d2(x) \<longleftrightarrow> \<not> p2(x)"
 
 thm d1_def d2_def
 
@@ -222,10 +222,10 @@
 (* A somewhat arcane homomorphism example *)
 
 definition semi_hom where
-  "semi_hom(prod, sum, h) <-> (ALL x y. h(prod(x, y)) = sum(h(x), h(y)))"
+  "semi_hom(prod, sum, h) \<longleftrightarrow> (\<forall>x y. h(prod(x, y)) = sum(h(x), h(y)))"
 
 lemma semi_hom_mult:
-  "semi_hom(prod, sum, h) ==> h(prod(x, y)) = sum(h(x), h(y))"
+  "semi_hom(prod, sum, h) \<Longrightarrow> h(prod(x, y)) = sum(h(x), h(y))"
   by (simp add: semi_hom_def)
 
 locale semi_hom_loc = prod: semi prod + sum: semi sum
@@ -242,7 +242,7 @@
 (* Referring to facts from within a context specification *)
 
 lemma
-  assumes x: "P <-> P"
+  assumes x: "P \<longleftrightarrow> P"
   notes y = x
   shows True ..
 
@@ -250,7 +250,7 @@
 section \<open>Theorem statements\<close>
 
 lemma (in lgrp) lcancel:
-  "x ** y = x ** z <-> y = z"
+  "x ** y = x ** z \<longleftrightarrow> y = z"
 proof
   assume "x ** y = x ** z"
   then have "inv(x) ** x ** y = inv(x) ** x ** z" by (simp add: assoc)
@@ -266,7 +266,7 @@
 begin
 
 lemma rcancel:
-  "y ** x = z ** x <-> y = z"
+  "y ** x = z ** x \<longleftrightarrow> y = z"
 proof
   assume "y ** x = z ** x"
   then have "y ** (x ** inv(x)) = z ** (x ** inv(x))"
@@ -322,7 +322,7 @@
 (* use of derived theorem *)
 
 lemma (in lgrp)
-  "y ** x = z ** x <-> y = z"
+  "y ** x = z ** x \<longleftrightarrow> y = z"
   apply (rule rcancel)
   done
 
@@ -372,7 +372,7 @@
 begin
 
 definition greater :: "'a => 'a => o" (infix ">>" 50) where
-  "x >> y <-> y << x"
+  "x >> y \<longleftrightarrow> y << x"
 
 end
 
@@ -392,7 +392,7 @@
 
 locale A5 =
   fixes A and B and C and D and E
-  assumes eq: "A <-> B <-> C <-> D <-> E"
+  assumes eq: "A \<longleftrightarrow> B \<longleftrightarrow> C \<longleftrightarrow> D \<longleftrightarrow> E"
 
 sublocale A5 < 1: A5 _ _ D E C
 print_facts
@@ -415,7 +415,7 @@
 
 locale trivial =
   fixes P and Q :: o
-  assumes Q: "P <-> P <-> Q"
+  assumes Q: "P \<longleftrightarrow> P \<longleftrightarrow> Q"
 begin
 
 lemma Q_triv: "Q" using Q by fast
@@ -494,28 +494,28 @@
 locale logic_o =
   fixes land (infixl "&&" 55)
     and lnot ("-- _" [60] 60)
-  assumes assoc_o: "(x && y) && z <-> x && (y && z)"
-    and notnot_o: "-- (-- x) <-> x"
+  assumes assoc_o: "(x && y) && z \<longleftrightarrow> x && (y && z)"
+    and notnot_o: "-- (-- x) \<longleftrightarrow> x"
 begin
 
 definition lor_o (infixl "||" 50) where
-  "x || y <-> --(-- x && -- y)"
+  "x || y \<longleftrightarrow> --(-- x && -- y)"
 
 end
 
-interpretation x: logic_o "op &" "Not"
-  where bool_logic_o: "x.lor_o(x, y) <-> x | y"
+interpretation x: logic_o "op \<and>" "Not"
+  where bool_logic_o: "x.lor_o(x, y) \<longleftrightarrow> x \<or> y"
 proof -
-  show bool_logic_o: "PROP logic_o(op &, Not)" by unfold_locales fast+
-  show "logic_o.lor_o(op &, Not, x, y) <-> x | y"
+  show bool_logic_o: "PROP logic_o(op \<and>, Not)" by unfold_locales fast+
+  show "logic_o.lor_o(op \<and>, Not, x, y) \<longleftrightarrow> x \<or> y"
     by (unfold logic_o.lor_o_def [OF bool_logic_o]) fast
 qed
 
 thm x.lor_o_def bool_logic_o
 
-lemma lor_triv: "z <-> z" ..
+lemma lor_triv: "z \<longleftrightarrow> z" ..
 
-lemma (in logic_o) lor_triv: "x || y <-> x || y" by fast
+lemma (in logic_o) lor_triv: "x || y \<longleftrightarrow> x || y" by fast
 
 thm lor_triv [where z = True] (* Check strict prefix. *)
   x.lor_triv
@@ -528,7 +528,7 @@
   assumes refl: "x \<sqsubseteq> x"
 begin
 
-definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y <-> x \<sqsubseteq> y & x ~= y"
+definition less (infix "\<sqsubset>" 50) where "x \<sqsubset> y \<longleftrightarrow> x \<sqsubseteq> y \<and> x \<noteq> y"
 
 end
 
@@ -536,8 +536,8 @@
   gle :: "'a => 'a => o" and gless :: "'a => 'a => o" and
   gle' :: "'a => 'a => o" and gless' :: "'a => 'a => o"
 where
-  grefl: "gle(x, x)" and gless_def: "gless(x, y) <-> gle(x, y) & x ~= y" and
-  grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) <-> gle'(x, y) & x ~= y"
+  grefl: "gle(x, x)" and gless_def: "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" and
+  grefl': "gle'(x, x)" and gless'_def: "gless'(x, y) \<longleftrightarrow> gle'(x, y) \<and> x \<noteq> y"
 
 text \<open>Setup\<close>
 
@@ -546,11 +546,11 @@
 lemmas less_thm = less_def
 end
 
-interpretation le: mixin gle where "reflexive.less(gle, x, y) <-> gless(x, y)"
+interpretation le: mixin gle where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin(gle)" by unfold_locales (rule grefl)
   note reflexive = this[unfolded mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
     by (simp add: reflexive.less_def[OF reflexive] gless_def)
 qed
 
@@ -565,7 +565,7 @@
   by unfold_locales
 
 thm le.less_thm2  (* rewrite morphism applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
   by (rule le.less_thm2)
 
 text \<open>Rewrite morphism does not leak to a side branch.\<close>
@@ -579,7 +579,7 @@
   by unfold_locales
 
 thm le.less_thm3  (* rewrite morphism not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y" by (rule le.less_thm3)
+lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y" by (rule le.less_thm3)
 
 text \<open>Rewrite morphism only available in original context\<close>
 
@@ -588,11 +588,11 @@
 locale mixin4_mixin = mixin4_base
 
 interpretation le: mixin4_mixin gle
-  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin4_mixin(gle)" by unfold_locales (rule grefl)
   note reflexive = this[unfolded mixin4_mixin_def mixin4_base_def mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
     by (simp add: reflexive.less_def[OF reflexive] gless_def)
 qed
 
@@ -610,7 +610,7 @@
   by unfold_locales (rule grefl')
 
 thm le4.less_thm4' (* rewrite morphism not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
   by (rule le4.less_thm4')
 
 text \<open>Inherited rewrite morphism applied to new theorem\<close>
@@ -620,11 +620,11 @@
 locale mixin5_inherited = mixin5_base
 
 interpretation le5: mixin5_base gle
-  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin5_base(gle)" by unfold_locales
   note reflexive = this[unfolded mixin5_base_def mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
     by (simp add: reflexive.less_def[OF reflexive] gless_def)
 qed
 
@@ -634,7 +634,7 @@
 lemmas (in mixin5_inherited) less_thm5 = less_def
 
 thm le5.less_thm5  (* rewrite morphism applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
   by (rule le5.less_thm5)
 
 text \<open>Rewrite morphism pushed down to existing inherited locale\<close>
@@ -648,18 +648,18 @@
 interpretation le6: mixin6_inherited gle
   by unfold_locales
 interpretation le6: mixin6_base gle
-  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin6_base(gle)" by unfold_locales
   note reflexive = this[unfolded mixin6_base_def mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
     by (simp add: reflexive.less_def[OF reflexive] gless_def)
 qed
 
 lemmas (in mixin6_inherited) less_thm6 = less_def
 
 thm le6.less_thm6  (* mixin applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
   by (rule le6.less_thm6)
 
 text \<open>Existing rewrite morphism inherited through sublocale relation\<close>
@@ -669,11 +669,11 @@
 locale mixin7_inherited = reflexive
 
 interpretation le7: mixin7_base gle
-  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin7_base(gle)" by unfold_locales
   note reflexive = this[unfolded mixin7_base_def mixin_def]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
     by (simp add: reflexive.less_def[OF reflexive] gless_def)
 qed
 
@@ -683,7 +683,7 @@
 lemmas (in mixin7_inherited) less_thm7 = less_def
 
 thm le7.less_thm7  (* before, rewrite morphism not applied *)
-lemma "reflexive.less(gle, x, y) <-> gle(x, y) & x ~= y"
+lemma "reflexive.less(gle, x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
   by (rule le7.less_thm7)
 
 sublocale mixin7_inherited < mixin7_base
@@ -692,7 +692,7 @@
 lemmas (in mixin7_inherited) less_thm7b = less_def
 
 thm le7.less_thm7b  (* after, mixin applied *)
-lemma "gless(x, y) <-> gle(x, y) & x ~= y"
+lemma "gless(x, y) \<longleftrightarrow> gle(x, y) \<and> x \<noteq> y"
   by (rule le7.less_thm7b)
 
 
@@ -764,11 +764,11 @@
 
 text \<open>Roundup applies rewrite morphisms at declaration level in DFS tree\<close>
 
-locale roundup = fixes x assumes true: "x <-> True"
+locale roundup = fixes x assumes true: "x \<longleftrightarrow> True"
 
-sublocale roundup \<subseteq> sub: roundup x where "x <-> True & True"
+sublocale roundup \<subseteq> sub: roundup x where "x \<longleftrightarrow> True \<and> True"
   apply unfold_locales apply (simp add: true) done
-lemma (in roundup) "True & True <-> True" by (rule sub.true)
+lemma (in roundup) "True \<and> True \<longleftrightarrow> True" by (rule sub.true)
 
 
 section \<open>Interpretation in named contexts\<close>
@@ -812,19 +812,19 @@
 proof
   {
     fix pand and pnot and por
-    assume passoc: "!!x y z. pand(pand(x, y), z) <-> pand(x, pand(y, z))"
-      and pnotnot: "!!x. pnot(pnot(x)) <-> x"
-      and por_def: "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))"
+    assume passoc: "\<And>x y z. pand(pand(x, y), z) \<longleftrightarrow> pand(x, pand(y, z))"
+      and pnotnot: "\<And>x. pnot(pnot(x)) \<longleftrightarrow> x"
+      and por_def: "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))"
     interpret loc: logic_o pand pnot
-      where por_eq: "!!x y. logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"  (* FIXME *)
+      where por_eq: "\<And>x y. logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)"  (* FIXME *)
     proof -
       show logic_o: "PROP logic_o(pand, pnot)" using passoc pnotnot by unfold_locales
       fix x y
-      show "logic_o.lor_o(pand, pnot, x, y) <-> por(x, y)"
+      show "logic_o.lor_o(pand, pnot, x, y) \<longleftrightarrow> por(x, y)"
         by (unfold logic_o.lor_o_def [OF logic_o]) (rule por_def [symmetric])
     qed
     print_interps logic_o
-    have "!!x y. por(x, y) <-> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
+    have "\<And>x y. por(x, y) \<longleftrightarrow> pnot(pand(pnot(x), pnot(y)))" by (rule loc.lor_o_def)
   }
 qed
 
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Locale_Test/Locale_Test2.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test2.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test2.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -9,11 +9,11 @@
 begin
 
 interpretation le1: mixin_thy_merge gle gle'
-  where "reflexive.less(gle, x, y) <-> gless(x, y)"
+  where "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
 proof -
   show "mixin_thy_merge(gle, gle')" by unfold_locales
   note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct1]
-  show "reflexive.less(gle, x, y) <-> gless(x, y)"
+  show "reflexive.less(gle, x, y) \<longleftrightarrow> gless(x, y)"
     by (simp add: reflexive.less_def[OF reflexive] gless_def)
 qed
 
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Locale_Test/Locale_Test3.thy
--- a/src/FOL/ex/Locale_Test/Locale_Test3.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Locale_Test/Locale_Test3.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -9,11 +9,11 @@
 begin
 
 interpretation le2: mixin_thy_merge gle gle'
-  where "reflexive.less(gle', x, y) <-> gless'(x, y)"
+  where "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
 proof -
   show "mixin_thy_merge(gle, gle')" by unfold_locales
   note reflexive = this[unfolded mixin_thy_merge_def, THEN conjunct2]
-  show "reflexive.less(gle', x, y) <-> gless'(x, y)"
+  show "reflexive.less(gle', x, y) \<longleftrightarrow> gless'(x, y)"
     by (simp add: reflexive.less_def[OF reflexive] gless'_def)
 qed
 
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Miniscope.thy
--- a/src/FOL/ex/Miniscope.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Miniscope.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -11,7 +11,6 @@
 imports FOL
 begin
 
-
 lemmas ccontr = FalseE [THEN classical]
 
 subsection \<open>Negation Normal Form\<close>
@@ -19,20 +18,20 @@
 subsubsection \<open>de Morgan laws\<close>
 
 lemma demorgans:
-  "~(P&Q) <-> ~P | ~Q"
-  "~(P|Q) <-> ~P & ~Q"
-  "~~P <-> P"
-  "!!P. ~(ALL x. P(x)) <-> (EX x. ~P(x))"
-  "!!P. ~(EX x. P(x)) <-> (ALL x. ~P(x))"
+  "\<not> (P \<and> Q) \<longleftrightarrow> \<not> P \<or> \<not> Q"
+  "\<not> (P \<or> Q) \<longleftrightarrow> \<not> P \<and> \<not> Q"
+  "\<not> \<not> P \<longleftrightarrow> P"
+  "\<And>P. \<not> (\<forall>x. P(x)) \<longleftrightarrow> (\<exists>x. \<not> P(x))"
+  "\<And>P. \<not> (\<exists>x. P(x)) \<longleftrightarrow> (\<forall>x. \<not> P(x))"
   by blast+
 
 (*** Removal of --> and <-> (positive and negative occurrences) ***)
 (*Last one is important for computing a compact CNF*)
 lemma nnf_simps:
-  "(P-->Q) <-> (~P | Q)"
-  "~(P-->Q) <-> (P & ~Q)"
-  "(P<->Q) <-> (~P | Q) & (~Q | P)"
-  "~(P<->Q) <-> (P | Q) & (~P | ~Q)"
+  "(P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
+  "\<not> (P \<longrightarrow> Q) \<longleftrightarrow> (P \<and> \<not> Q)"
+  "(P \<longleftrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q) \<and> (\<not> Q \<or> P)"
+  "\<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<or> Q) \<and> (\<not> P \<or> \<not> Q)"
   by blast+
 
 
@@ -41,24 +40,24 @@
 subsubsection \<open>Pushing in the existential quantifiers\<close>
 
 lemma ex_simps:
-  "(EX x. P) <-> P"
-  "!!P Q. (EX x. P(x) & Q) <-> (EX x. P(x)) & Q"
-  "!!P Q. (EX x. P & Q(x)) <-> P & (EX x. Q(x))"
-  "!!P Q. (EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
-  "!!P Q. (EX x. P(x) | Q) <-> (EX x. P(x)) | Q"
-  "!!P Q. (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
+  "(\<exists>x. P) \<longleftrightarrow> P"
+  "\<And>P Q. (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
+  "\<And>P Q. (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
+  "\<And>P Q. (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
+  "\<And>P Q. (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
+  "\<And>P Q. (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
   by blast+
 
 
 subsubsection \<open>Pushing in the universal quantifiers\<close>
 
 lemma all_simps:
-  "(ALL x. P) <-> P"
-  "!!P Q. (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
-  "!!P Q. (ALL x. P(x) & Q) <-> (ALL x. P(x)) & Q"
-  "!!P Q. (ALL x. P & Q(x)) <-> P & (ALL x. Q(x))"
-  "!!P Q. (ALL x. P(x) | Q) <-> (ALL x. P(x)) | Q"
-  "!!P Q. (ALL x. P | Q(x)) <-> P | (ALL x. Q(x))"
+  "(\<forall>x. P) \<longleftrightarrow> P"
+  "\<And>P Q. (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
+  "\<And>P Q. (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
+  "\<And>P Q. (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
+  "\<And>P Q. (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
+  "\<And>P Q. (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<forall>x. Q(x))"
   by blast+
 
 lemmas mini_simps = demorgans nnf_simps ex_simps all_simps
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Nat.thy
--- a/src/FOL/ex/Nat.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Nat.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -29,7 +29,7 @@
 
 subsection \<open>Proofs about the natural numbers\<close>
 
-lemma Suc_n_not_n: "Suc(k) ~= k"
+lemma Suc_n_not_n: "Suc(k) \<noteq> k"
 apply (rule_tac n = k in induct)
 apply (rule notI)
 apply (erule Suc_neq_0)
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Prolog.thy
--- a/src/FOL/ex/Prolog.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Prolog.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -83,7 +83,7 @@
 
 (*?x has 16, ?y has 32;  rev(?y,?w) requires 561 (rather large) inferences
   total inferences = 2 + 1 + 17 + 561 = 581*)
-schematic_goal "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x & app(?x,?x,?y) & rev(?y,?w)"
+schematic_goal "a:b:c:d:e:f:g:h:i:j:k:l:m:n:o:p:Nil = ?x \<and> app(?x,?x,?y) \<and> rev(?y,?w)"
 apply (tactic \<open>
   DEPTH_SOLVE (resolve_tac @{context} ([@{thm refl}, @{thm conjI}] @ @{thms rules}) 1)\<close>)
 done
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Propositional_Cla.thy
--- a/src/FOL/ex/Propositional_Cla.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Propositional_Cla.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -9,109 +9,112 @@
 imports FOL
 begin
 
-text \<open>commutative laws of @{text "&"} and @{text "|"}\<close>
+text \<open>commutative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
 
-lemma "P & Q  -->  Q & P"
+lemma "P \<and> Q \<longrightarrow> Q \<and> P"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "P | Q  -->  Q | P"
+lemma "P \<or> Q \<longrightarrow> Q \<or> P"
   by fast
 
 
-text \<open>associative laws of @{text "&"} and @{text "|"}\<close>
-lemma "(P & Q) & R  -->  P & (Q & R)"
+text \<open>associative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
   by fast
 
-lemma "(P | Q) | R  -->  P | (Q | R)"
+lemma "(P \<or> Q) \<or> R \<longrightarrow>  P \<or> (Q \<or> R)"
   by fast
 
 
-text \<open>distributive laws of @{text "&"} and @{text "|"}\<close>
-lemma "(P & Q) | R  --> (P | R) & (Q | R)"
+text \<open>distributive laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
   by fast
 
-lemma "(P | R) & (Q | R)  --> (P & Q) | R"
+lemma "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R"
   by fast
 
-lemma "(P | Q) & R  --> (P & R) | (Q & R)"
+lemma "(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)"
   by fast
 
-lemma "(P & R) | (Q & R)  --> (P | Q) & R"
+lemma "(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R"
   by fast
 
 
 text \<open>Laws involving implication\<close>
 
-lemma "(P-->R) & (Q-->R) <-> (P|Q --> R)"
+lemma "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)"
   by fast
 
-lemma "(P & Q --> R) <-> (P--> (Q-->R))"
+lemma "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
   by fast
 
-lemma "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
+lemma "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R"
   by fast
 
-lemma "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
+lemma "\<not> (P \<longrightarrow> R) \<longrightarrow> \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)"
   by fast
 
-lemma "(P --> Q & R) <-> (P-->Q)  &  (P-->R)"
+lemma "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
   by fast
 
 
 text \<open>Propositions-as-types\<close>
 
 -- \<open>The combinator K\<close>
-lemma "P --> (Q --> P)"
+lemma "P \<longrightarrow> (Q \<longrightarrow> P)"
   by fast
 
 -- \<open>The combinator S\<close>
-lemma "(P-->Q-->R)  --> (P-->Q) --> (P-->R)"
+lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)"
   by fast
 
 
 -- \<open>Converse is classical\<close>
-lemma "(P-->Q) | (P-->R)  -->  (P --> Q | R)"
+lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
   by fast
 
-lemma "(P-->Q)  -->  (~Q --> ~P)"
+lemma "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
   by fast
 
 
 text \<open>Schwichtenberg's examples (via T. Nipkow)\<close>
 
-lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
+lemma stab_imp: "(((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q"
   by fast
 
 lemma stab_to_peirce:
-  "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
-                              --> ((P --> Q) --> P) --> P"
+  "(((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> (((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q)
+    \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
   by fast
 
-lemma peirce_imp1: "(((Q --> R) --> Q) --> Q)  
-                --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
-  by fast
-  
-lemma peirce_imp2: "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
+lemma peirce_imp1:
+  "(((Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> Q)
+    \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q) \<longrightarrow> P \<longrightarrow> Q"
   by fast
 
-lemma mints: "((((P --> Q) --> P) --> P) --> Q) --> Q"
+lemma peirce_imp2: "(((P \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> ((P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P"
+  by fast
+
+lemma mints: "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
   by fast
 
-lemma mints_solovev: "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
+lemma mints_solovev: "(P \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R"
   by fast
 
-lemma tatsuta: "(((P7 --> P1) --> P10) --> P4 --> P5)  
-  --> (((P8 --> P2) --> P9) --> P3 --> P10)  
-  --> (P1 --> P8) --> P6 --> P7  
-  --> (((P3 --> P2) --> P9) --> P4)  
-  --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
+lemma tatsuta:
+  "(((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
+  \<longrightarrow> (((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
+  \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7
+  \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
+  \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P5"
   by fast
 
-lemma tatsuta1: "(((P8 --> P2) --> P9) --> P3 --> P10)  
-  --> (((P3 --> P2) --> P9) --> P4)  
-  --> (((P6 --> P1) --> P2) --> P9)  
-  --> (((P7 --> P1) --> P10) --> P4 --> P5)  
-  --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
+lemma tatsuta1:
+  "(((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
+  \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
+  \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9)
+  \<longrightarrow> (((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
+  \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7 \<longrightarrow> P5"
   by fast
 
 end
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Propositional_Int.thy
--- a/src/FOL/ex/Propositional_Int.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Propositional_Int.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -9,109 +9,112 @@
 imports IFOL
 begin
 
-text \<open>commutative laws of @{text "&"} and @{text "|"}\<close>
+text \<open>commutative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
 
-lemma "P & Q  -->  Q & P"
+lemma "P \<and> Q \<longrightarrow> Q \<and> P"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "P | Q  -->  Q | P"
+lemma "P \<or> Q \<longrightarrow> Q \<or> P"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
-text \<open>associative laws of @{text "&"} and @{text "|"}\<close>
-lemma "(P & Q) & R  -->  P & (Q & R)"
+text \<open>associative laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+lemma "(P \<and> Q) \<and> R \<longrightarrow> P \<and> (Q \<and> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(P | Q) | R  -->  P | (Q | R)"
+lemma "(P \<or> Q) \<or> R \<longrightarrow> P \<or> (Q \<or> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
-text \<open>distributive laws of @{text "&"} and @{text "|"}\<close>
-lemma "(P & Q) | R  --> (P | R) & (Q | R)"
+text \<open>distributive laws of @{text "\<and>"} and @{text "\<or>"}\<close>
+lemma "(P \<and> Q) \<or> R \<longrightarrow> (P \<or> R) \<and> (Q \<or> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(P | R) & (Q | R)  --> (P & Q) | R"
+lemma "(P \<or> R) \<and> (Q \<or> R) \<longrightarrow> (P \<and> Q) \<or> R"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(P | Q) & R  --> (P & R) | (Q & R)"
+lemma "(P \<or> Q) \<and> R \<longrightarrow> (P \<and> R) \<or> (Q \<and> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(P & R) | (Q & R)  --> (P | Q) & R"
+lemma "(P \<and> R) \<or> (Q \<and> R) \<longrightarrow> (P \<or> Q) \<and> R"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text \<open>Laws involving implication\<close>
 
-lemma "(P-->R) & (Q-->R) <-> (P|Q --> R)"
+lemma "(P \<longrightarrow> R) \<and> (Q \<longrightarrow> R) \<longleftrightarrow> (P \<or> Q \<longrightarrow> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(P & Q --> R) <-> (P--> (Q-->R))"
+lemma "(P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "((P-->R)-->R) --> ((Q-->R)-->R) --> (P&Q-->R) --> R"
+lemma "((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> ((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<longrightarrow> R) \<longrightarrow> R"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "~(P-->R) --> ~(Q-->R) --> ~(P&Q-->R)"
+lemma "\<not> (P \<longrightarrow> R) \<longrightarrow> \<not> (Q \<longrightarrow> R) \<longrightarrow> \<not> (P \<and> Q \<longrightarrow> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(P --> Q & R) <-> (P-->Q)  &  (P-->R)"
+lemma "(P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text \<open>Propositions-as-types\<close>
 
 -- \<open>The combinator K\<close>
-lemma "P --> (Q --> P)"
+lemma "P \<longrightarrow> (Q \<longrightarrow> P)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 -- \<open>The combinator S\<close>
-lemma "(P-->Q-->R)  --> (P-->Q) --> (P-->R)"
+lemma "(P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q) \<longrightarrow> (P \<longrightarrow> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 -- \<open>Converse is classical\<close>
-lemma "(P-->Q) | (P-->R)  -->  (P --> Q | R)"
+lemma "(P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longrightarrow> (P \<longrightarrow> Q \<or> R)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(P-->Q)  -->  (~Q --> ~P)"
+lemma "(P \<longrightarrow> Q) \<longrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text \<open>Schwichtenberg's examples (via T. Nipkow)\<close>
 
-lemma stab_imp: "(((Q-->R)-->R)-->Q) --> (((P-->Q)-->R)-->R)-->P-->Q"
+lemma stab_imp: "(((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 lemma stab_to_peirce:
-  "(((P --> R) --> R) --> P) --> (((Q --> R) --> R) --> Q)  
-                              --> ((P --> Q) --> P) --> P"
+  "(((P \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> (((Q \<longrightarrow> R) \<longrightarrow> R) \<longrightarrow> Q)
+    \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma peirce_imp1: "(((Q --> R) --> Q) --> Q)  
-                --> (((P --> Q) --> R) --> P --> Q) --> P --> Q"
-  by (tactic "IntPr.fast_tac @{context} 1")
-  
-lemma peirce_imp2: "(((P --> R) --> P) --> P) --> ((P --> Q --> R) --> P) --> P"
+lemma peirce_imp1:
+  "(((Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> Q)
+    \<longrightarrow> (((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> P \<longrightarrow> Q) \<longrightarrow> P \<longrightarrow> Q"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma mints: "((((P --> Q) --> P) --> P) --> Q) --> Q"
+lemma peirce_imp2: "(((P \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> ((P \<longrightarrow> Q \<longrightarrow> R) \<longrightarrow> P) \<longrightarrow> P"
+  by (tactic "IntPr.fast_tac @{context} 1")
+
+lemma mints: "((((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P) \<longrightarrow> Q) \<longrightarrow> Q"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma mints_solovev: "(P --> (Q --> R) --> Q) --> ((P --> Q) --> R) --> R"
+lemma mints_solovev: "(P \<longrightarrow> (Q \<longrightarrow> R) \<longrightarrow> Q) \<longrightarrow> ((P \<longrightarrow> Q) \<longrightarrow> R) \<longrightarrow> R"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma tatsuta: "(((P7 --> P1) --> P10) --> P4 --> P5)  
-  --> (((P8 --> P2) --> P9) --> P3 --> P10)  
-  --> (P1 --> P8) --> P6 --> P7  
-  --> (((P3 --> P2) --> P9) --> P4)  
-  --> (P1 --> P3) --> (((P6 --> P1) --> P2) --> P9) --> P5"
+lemma tatsuta:
+  "(((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
+  \<longrightarrow> (((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
+  \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7
+  \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
+  \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P5"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma tatsuta1: "(((P8 --> P2) --> P9) --> P3 --> P10)  
-  --> (((P3 --> P2) --> P9) --> P4)  
-  --> (((P6 --> P1) --> P2) --> P9)  
-  --> (((P7 --> P1) --> P10) --> P4 --> P5)  
-  --> (P1 --> P3) --> (P1 --> P8) --> P6 --> P7 --> P5"
+lemma tatsuta1:
+  "(((P8 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P3 \<longrightarrow> P10)
+  \<longrightarrow> (((P3 \<longrightarrow> P2) \<longrightarrow> P9) \<longrightarrow> P4)
+  \<longrightarrow> (((P6 \<longrightarrow> P1) \<longrightarrow> P2) \<longrightarrow> P9)
+  \<longrightarrow> (((P7 \<longrightarrow> P1) \<longrightarrow> P10) \<longrightarrow> P4 \<longrightarrow> P5)
+  \<longrightarrow> (P1 \<longrightarrow> P3) \<longrightarrow> (P1 \<longrightarrow> P8) \<longrightarrow> P6 \<longrightarrow> P7 \<longrightarrow> P5"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 end
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Quantifiers_Cla.thy
--- a/src/FOL/ex/Quantifiers_Cla.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Quantifiers_Cla.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -9,92 +9,92 @@
 imports FOL
 begin
 
-lemma "(ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
+lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>y x. P(x,y))"
   by fast
 
-lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
+lemma "(\<exists>x y. P(x,y)) \<longrightarrow> (\<exists>y x. P(x,y))"
   by fast
 
 
--- \<open>Converse is false\<close>
-lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
+text \<open>Converse is false.\<close>
+lemma "(\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
   by fast
 
-lemma "(ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
+lemma "(\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
   by fast
 
 
-lemma "(ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
+lemma "(\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
   by fast
 
 
-text \<open>Some harder ones\<close>
+text \<open>Some harder ones.\<close>
 
-lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
+lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
   by fast
 
--- \<open>Converse is false\<close>
-lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
+-- \<open>Converse is false.\<close>
+lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
   by fast
 
 
-text \<open>Basic test of quantifier reasoning\<close>
+text \<open>Basic test of quantifier reasoning.\<close>
 
 -- \<open>TRUE\<close>
-lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
+lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
   by fast
 
-lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
+lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
   by fast
 
 
 text \<open>The following should fail, as they are false!\<close>
 
-lemma "(ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
+lemma "(\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
   apply fast?
   oops
 
-lemma "(EX x. Q(x))  -->  (ALL x. Q(x))"
+lemma "(\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
   apply fast?
   oops
 
-schematic_goal "P(?a) --> (ALL x. P(x))"
+schematic_goal "P(?a) \<longrightarrow> (\<forall>x. P(x))"
   apply fast?
   oops
 
-schematic_goal "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_goal "(P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
   apply fast?
   oops
 
 
 text \<open>Back to things that are provable \dots\<close>
 
-lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
+lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
   by fast
 
--- \<open>An example of why exI should be delayed as long as possible\<close>
-lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
+text \<open>An example of why @{text exI} should be delayed as long as possible.\<close>
+lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
   by fast
 
-schematic_goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_goal "(\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)"
   by fast
 
-lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
+lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
   by fast
 
 
 text \<open>Some slow ones\<close>
 
--- \<open>Principia Mathematica *11.53\<close>
-lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
+text \<open>Principia Mathematica *11.53\<close>
+lemma "(\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
   by fast
 
 (*Principia Mathematica *11.55  *)
-lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
+lemma "(\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
   by fast
 
 (*Principia Mathematica *11.61  *)
-lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
+lemma "(\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
   by fast
 
 end
diff -r d40cbf1f37c9 -r b8d375aee0df src/FOL/ex/Quantifiers_Int.thy
--- a/src/FOL/ex/Quantifiers_Int.thy	Mon Oct 19 20:31:13 2015 +0200
+++ b/src/FOL/ex/Quantifiers_Int.thy	Mon Oct 19 23:00:07 2015 +0200
@@ -9,92 +9,92 @@
 imports IFOL
 begin
 
-lemma "(ALL x y. P(x,y))  -->  (ALL y x. P(x,y))"
+lemma "(\<forall>x y. P(x,y)) \<longrightarrow> (\<forall>y x. P(x,y))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(EX x y. P(x,y)) --> (EX y x. P(x,y))"
+lemma "(\<exists>x y. P(x,y)) \<longrightarrow> (\<exists>y x. P(x,y))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 -- \<open>Converse is false\<close>
-lemma "(ALL x. P(x)) | (ALL x. Q(x)) --> (ALL x. P(x) | Q(x))"
+lemma "(\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(ALL x. P-->Q(x))  <->  (P--> (ALL x. Q(x)))"
+lemma "(\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
-lemma "(ALL x. P(x)-->Q)  <->  ((EX x. P(x)) --> Q)"
+lemma "(\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text \<open>Some harder ones\<close>
 
-lemma "(EX x. P(x) | Q(x)) <-> (EX x. P(x)) | (EX x. Q(x))"
+lemma "(\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 -- \<open>Converse is false\<close>
-lemma "(EX x. P(x)&Q(x)) --> (EX x. P(x))  &  (EX x. Q(x))"
+lemma "(\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text \<open>Basic test of quantifier reasoning\<close>
 
 -- \<open>TRUE\<close>
-lemma "(EX y. ALL x. Q(x,y)) -->  (ALL x. EX y. Q(x,y))"
+lemma "(\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
+lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text \<open>The following should fail, as they are false!\<close>
 
-lemma "(ALL x. EX y. Q(x,y))  -->  (EX y. ALL x. Q(x,y))"
+lemma "(\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
   apply (tactic "IntPr.fast_tac @{context} 1")?
   oops
 
-lemma "(EX x. Q(x))  -->  (ALL x. Q(x))"
+lemma "(\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
   apply (tactic "IntPr.fast_tac @{context} 1")?
   oops
 
-schematic_goal "P(?a) --> (ALL x. P(x))"
+schematic_goal "P(?a) \<longrightarrow> (\<forall>x. P(x))"
   apply (tactic "IntPr.fast_tac @{context} 1")?
   oops
 
-schematic_goal "(P(?a) --> (ALL x. Q(x))) --> (ALL x. P(x) --> Q(x))"
+schematic_goal "(P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
   apply (tactic "IntPr.fast_tac @{context} 1")?
   oops
 
 
 text \<open>Back to things that are provable \dots\<close>
 
-lemma "(ALL x. P(x)-->Q(x)) & (EX x. P(x)) --> (EX x. Q(x))"
+lemma "(\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 -- \<open>An example of why exI should be delayed as long as possible\<close>
-lemma "(P --> (EX x. Q(x))) & P --> (EX x. Q(x))"
+lemma "(P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-schematic_goal "(ALL x. P(x)-->Q(f(x))) & (ALL x. Q(x)-->R(g(x))) & P(d) --> R(?a)"
+schematic_goal "(\<forall>x. P(x) \<longrightarrow> Q(f(x))) \<and> (\<forall>x. Q(x) \<longrightarrow> R(g(x))) \<and> P(d) \<longrightarrow> R(?a)"
   by (tactic "IntPr.fast_tac @{context} 1")
 
-lemma "(ALL x. Q(x))  -->  (EX x. Q(x))"
+lemma "(\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 
 text \<open>Some slow ones\<close>
 
 -- \<open>Principia Mathematica *11.53\<close>
-lemma "(ALL x y. P(x) --> Q(y)) <-> ((EX x. P(x)) --> (ALL y. Q(y)))"
+lemma "(\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 (*Principia Mathematica *11.55  *)
-lemma "(EX x y. P(x) & Q(x,y)) <-> (EX x. P(x) & (EX y. Q(x,y)))"
+lemma "(\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 (*Principia Mathematica *11.61  *)
-lemma "(EX y. ALL x. P(x) --> Q(x,y)) --> (ALL x. P(x) --> (EX y. Q(x,y)))"
+lemma "(\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
   by (tactic "IntPr.fast_tac @{context} 1")
 
 end