# HG changeset patch
# User wenzelm
# Date 1444503099 -7200
# Node ID 538100cc4399e81ad07b3e70a652a4fffee99122
# Parent  9f5145281888b637c3cc8e5669821d840356c44e
more symbols;

diff -r 9f5145281888 -r 538100cc4399 src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/ILL.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -10,16 +10,16 @@
 consts
   Trueprop       :: "two_seqi"
 
-  tens :: "[o, o] => o"        (infixr "><" 35)
-  limp :: "[o, o] => o"        (infixr "-o" 45)
-  liff :: "[o, o] => o"        (infixr "o-o" 45)
-  FShriek :: "o => o"          ("! _" [100] 1000)
-  lconj :: "[o, o] => o"       (infixr "&&" 35)
-  ldisj :: "[o, o] => o"       (infixr "++" 35)
+  tens :: "[o, o] \<Rightarrow> o"        (infixr "><" 35)
+  limp :: "[o, o] \<Rightarrow> o"        (infixr "-o" 45)
+  liff :: "[o, o] \<Rightarrow> o"        (infixr "o-o" 45)
+  FShriek :: "o \<Rightarrow> o"          ("! _" [100] 1000)
+  lconj :: "[o, o] \<Rightarrow> o"       (infixr "&&" 35)
+  ldisj :: "[o, o] \<Rightarrow> o"       (infixr "++" 35)
   zero :: "o"                  ("0")
   top :: "o"                   ("1")
   eye :: "o"                   ("I")
-  aneg :: "o=>o"               ("~_")
+  aneg :: "o\<Rightarrow>o"               ("~_")
 
 
   (* context manipulation *)
@@ -62,67 +62,67 @@
 
   (* RULES THAT DO NOT DIVIDE CONTEXT *)
 
-derelict:   "$F, A, $G |- C ==> $F, !A, $G |- C" and
+derelict:   "$F, A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and
   (* unfortunately, this one removes !A  *)
 
-contract:  "$F, !A, !A, $G |- C ==> $F, !A, $G |- C" and
+contract:  "$F, !A, !A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and
 
-weaken:     "$F, $G |- C ==> $G, !A, $F |- C" and
+weaken:     "$F, $G |- C \<Longrightarrow> $G, !A, $F |- C" and
   (* weak form of weakening, in practice just to clean context *)
   (* weaken and contract not needed (CHECK)  *)
 
-promote2:        "promaux{ || $H || B} ==> $H |- !B" and
+promote2:        "promaux{ || $H || B} \<Longrightarrow> $H |- !B" and
 promote1:        "promaux{!A, $G || $H || B}
-                  ==> promaux {$G || $H, !A || B}" and
-promote0:        "$G |- A ==> promaux {$G || || A}" and
+                  \<Longrightarrow> promaux {$G || $H, !A || B}" and
+promote0:        "$G |- A \<Longrightarrow> promaux {$G || || A}" and
 
 
 
-tensl:     "$H, A, B, $G |- C ==> $H, A >< B, $G |- C" and
+tensl:     "$H, A, B, $G |- C \<Longrightarrow> $H, A >< B, $G |- C" and
 
-impr:      "A, $F |- B ==> $F |- A -o B" and
+impr:      "A, $F |- B \<Longrightarrow> $F |- A -o B" and
 
-conjr:           "[| $F |- A ;
-                 $F |- B |]
-                ==> $F |- (A && B)" and
+conjr:           "\<lbrakk>$F |- A ;
+                 $F |- B\<rbrakk>
+                \<Longrightarrow> $F |- (A && B)" and
 
-conjll:          "$G, A, $H |- C ==> $G, A && B, $H |- C" and
+conjll:          "$G, A, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and
 
-conjlr:          "$G, B, $H |- C ==> $G, A && B, $H |- C" and
+conjlr:          "$G, B, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and
 
-disjrl:          "$G |- A ==> $G |- A ++ B" and
-disjrr:          "$G |- B ==> $G |- A ++ B" and
-disjl:           "[| $G, A, $H |- C ;
-                     $G, B, $H |- C |]
-                 ==> $G, A ++ B, $H |- C" and
+disjrl:          "$G |- A \<Longrightarrow> $G |- A ++ B" and
+disjrr:          "$G |- B \<Longrightarrow> $G |- A ++ B" and
+disjl:           "\<lbrakk>$G, A, $H |- C ;
+                   $G, B, $H |- C\<rbrakk>
+                 \<Longrightarrow> $G, A ++ B, $H |- C" and
 
 
       (* RULES THAT DIVIDE CONTEXT *)
 
-tensr:           "[| $F, $J :=: $G;
-                     $F |- A ;
-                     $J |- B     |]
-                     ==> $G |- A >< B" and
+tensr:           "\<lbrakk>$F, $J :=: $G;
+                   $F |- A ;
+                   $J |- B\<rbrakk>
+                     \<Longrightarrow> $G |- A >< B" and
 
-impl:            "[| $G, $F :=: $J, $H ;
-                     B, $F |- C ;
-                        $G |- A |]
-                     ==> $J, A -o B, $H |- C" and
+impl:            "\<lbrakk>$G, $F :=: $J, $H ;
+                   B, $F |- C ;
+                   $G |- A\<rbrakk>
+                     \<Longrightarrow> $J, A -o B, $H |- C" and
 
 
-cut: " [| $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
-          $H1, $H2, $H3, $H4 |- A ;
-          $J1, $J2, A, $J3, $J4 |- B |]  ==> $F |- B" and
+cut: "\<lbrakk> $J1, $H1, $J2, $H3, $J3, $H2, $J4, $H4 :=: $F ;
+        $H1, $H2, $H3, $H4 |- A ;
+        $J1, $J2, A, $J3, $J4 |- B\<rbrakk> \<Longrightarrow> $F |- B" and
 
 
   (* CONTEXT RULES *)
 
 context1:     "$G :=: $G" and
-context2:     "$F, $G :=: $H, !A, $G ==> $F, A, $G :=: $H, !A, $G" and
-context3:     "$F, $G :=: $H, $J ==> $F, A, $G :=: $H, A, $J" and
-context4a:    "$F :=: $H, $G ==> $F :=: $H, !A, $G" and
-context4b:    "$F, $H :=: $G ==> $F, !A, $H :=: $G" and
-context5:     "$F, $G :=: $H ==> $G, $F :=: $H"
+context2:     "$F, $G :=: $H, !A, $G \<Longrightarrow> $F, A, $G :=: $H, !A, $G" and
+context3:     "$F, $G :=: $H, $J \<Longrightarrow> $F, A, $G :=: $H, A, $J" and
+context4a:    "$F :=: $H, $G \<Longrightarrow> $F :=: $H, !A, $G" and
+context4b:    "$F, $H :=: $G \<Longrightarrow> $F, !A, $H :=: $G" and
+context5:     "$F, $G :=: $H \<Longrightarrow> $G, $F :=: $H"
 
 text "declarations for lazy classical reasoning:"
 lemmas [safe] =
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/ILL_predlog.thy
--- a/src/Sequents/ILL_predlog.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/ILL_predlog.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -5,26 +5,25 @@
 typedecl plf
 
 consts
-  conj :: "[plf,plf] => plf"   (infixr "&" 35)
-  disj :: "[plf,plf] => plf"   (infixr "|" 35)
-  impl :: "[plf,plf] => plf"   (infixr ">" 35)
-  eq :: "[plf,plf] => plf"   (infixr "=" 35)
+  conj :: "[plf,plf] \<Rightarrow> plf"   (infixr "&" 35)
+  disj :: "[plf,plf] \<Rightarrow> plf"   (infixr "|" 35)
+  impl :: "[plf,plf] \<Rightarrow> plf"   (infixr ">" 35)
+  eq :: "[plf,plf] \<Rightarrow> plf"   (infixr "=" 35)
   ff :: "plf"    ("ff")
 
-  PL    :: "plf => o"      ("[* / _ / *]" [] 100)
+  PL    :: "plf \<Rightarrow> o"      ("[* / _ / *]" [] 100)
 
 syntax
-  "_NG" :: "plf => plf"   ("- _ " [50] 55)
+  "_NG" :: "plf \<Rightarrow> plf"   ("- _ " [50] 55)
 
 translations
+  "[* A & B *]" \<rightleftharpoons> "[*A*] && [*B*]"
+  "[* A | B *]" \<rightleftharpoons> "![*A*] ++ ![*B*]"
+  "[* - A *]" \<rightleftharpoons> "[*A > ff*]"
+  "[* ff *]" \<rightleftharpoons> "0"
+  "[* A = B *]" \<rightharpoonup> "[* (A > B) & (B > A) *]"
 
-  "[* A & B *]" == "[*A*] && [*B*]"
-  "[* A | B *]" == "![*A*] ++ ![*B*]"
-  "[* - A *]" == "[*A > ff*]"
-  "[* ff *]" == "0"
-  "[* A = B *]" => "[* (A > B) & (B > A) *]"
-
-  "[* A > B *]" == "![*A*] -o [*B*]"
+  "[* A > B *]" \<rightleftharpoons> "![*A*] -o [*B*]"
 
 (* another translations for linear implication:
   "[* A > B *]" == "!([*A*] -o [*B*])" *)
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -3,7 +3,7 @@
     Copyright   1993  University of Cambridge
 
 Axiom to express monotonicity (a variant of the deduction theorem).  Makes the
-link between |- and ==>, needed for instance to prove imp_cong.
+link between |- and \<Longrightarrow>, needed for instance to prove imp_cong.
 
 Axiom left_cong allows the simplifier to use left-side formulas.  Ideally it
 should be derived from lower-level axioms.
@@ -17,111 +17,111 @@
 begin
 
 axiomatization where
-  monotonic:  "($H |- P ==> $H |- Q) ==> $H, P |- Q" and
+  monotonic:  "($H |- P \<Longrightarrow> $H |- Q) \<Longrightarrow> $H, P |- Q" and
 
-  left_cong:  "[| P == P';  |- P' ==> ($H |- $F) == ($H' |- $F') |]
-               ==> (P, $H |- $F) == (P', $H' |- $F')"
+  left_cong:  "\<lbrakk>P == P';  |- P' \<Longrightarrow> ($H |- $F) \<equiv> ($H' |- $F')\<rbrakk>
+               \<Longrightarrow> (P, $H |- $F) \<equiv> (P', $H' |- $F')"
 
 
 subsection \<open>Rewrite rules\<close>
 
 lemma conj_simps:
-  "|- P & True <-> P"
-  "|- True & P <-> P"
-  "|- P & False <-> False"
-  "|- False & P <-> False"
-  "|- P & P <-> P"
-  "|- P & P & Q <-> P & Q"
-  "|- P & ~P <-> False"
-  "|- ~P & P <-> False"
-  "|- (P & Q) & R <-> P & (Q & R)"
+  "|- P \<and> True \<longleftrightarrow> P"
+  "|- True \<and> P \<longleftrightarrow> P"
+  "|- P \<and> False \<longleftrightarrow> False"
+  "|- False \<and> P \<longleftrightarrow> False"
+  "|- P \<and> P \<longleftrightarrow> P"
+  "|- P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q"
+  "|- P \<and> \<not> P \<longleftrightarrow> False"
+  "|- \<not> P \<and> P \<longleftrightarrow> False"
+  "|- (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
   by (fast add!: subst)+
 
 lemma disj_simps:
-  "|- P | True <-> True"
-  "|- True | P <-> True"
-  "|- P | False <-> P"
-  "|- False | P <-> P"
-  "|- P | P <-> P"
-  "|- P | P | Q <-> P | Q"
-  "|- (P | Q) | R <-> P | (Q | R)"
+  "|- P \<or> True \<longleftrightarrow> True"
+  "|- True \<or> P \<longleftrightarrow> True"
+  "|- P \<or> False \<longleftrightarrow> P"
+  "|- False \<or> P \<longleftrightarrow> P"
+  "|- P \<or> P \<longleftrightarrow> P"
+  "|- P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q"
+  "|- (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
   by (fast add!: subst)+
 
 lemma not_simps:
-  "|- ~ False <-> True"
-  "|- ~ True <-> False"
+  "|- \<not> False \<longleftrightarrow> True"
+  "|- \<not> True \<longleftrightarrow> False"
   by (fast add!: subst)+
 
 lemma imp_simps:
-  "|- (P --> False) <-> ~P"
-  "|- (P --> True) <-> True"
-  "|- (False --> P) <-> True"
-  "|- (True --> P) <-> P"
-  "|- (P --> P) <-> True"
-  "|- (P --> ~P) <-> ~P"
+  "|- (P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
+  "|- (P \<longrightarrow> True) \<longleftrightarrow> True"
+  "|- (False \<longrightarrow> P) \<longleftrightarrow> True"
+  "|- (True \<longrightarrow> P) \<longleftrightarrow> P"
+  "|- (P \<longrightarrow> P) \<longleftrightarrow> True"
+  "|- (P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P"
   by (fast add!: subst)+
 
 lemma iff_simps:
-  "|- (True <-> P) <-> P"
-  "|- (P <-> True) <-> P"
-  "|- (P <-> P) <-> True"
-  "|- (False <-> P) <-> ~P"
-  "|- (P <-> False) <-> ~P"
+  "|- (True \<longleftrightarrow> P) \<longleftrightarrow> P"
+  "|- (P \<longleftrightarrow> True) \<longleftrightarrow> P"
+  "|- (P \<longleftrightarrow> P) \<longleftrightarrow> True"
+  "|- (False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P"
+  "|- (P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P"
   by (fast add!: subst)+
 
 lemma quant_simps:
-  "!!P. |- (ALL x. P) <-> P"
-  "!!P. |- (ALL x. x=t --> P(x)) <-> P(t)"
-  "!!P. |- (ALL x. t=x --> P(x)) <-> P(t)"
-  "!!P. |- (EX x. P) <-> P"
-  "!!P. |- (EX x. x=t & P(x)) <-> P(t)"
-  "!!P. |- (EX x. t=x & P(x)) <-> P(t)"
+  "\<And>P. |- (\<forall>x. P) \<longleftrightarrow> P"
+  "\<And>P. |- (\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+  "\<And>P. |- (\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+  "\<And>P. |- (\<exists>x. P) \<longleftrightarrow> P"
+  "\<And>P. |- (\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)"
+  "\<And>P. |- (\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)"
   by (fast add!: subst)+
 
 
 subsection \<open>Miniscoping: pushing quantifiers in\<close>
 
 text \<open>
-  We do NOT distribute of ALL over &, or dually that of EX over |
+  We do NOT distribute of \<forall> over \<and>, or dually that of \<exists> over \<or>
   Baaz and Leitsch, On Skolemization and Proof Complexity (1994)
   show that this step can increase proof length!
 \<close>
 
 text \<open>existential miniscoping\<close>
 lemma ex_simps:
-  "!!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) <-> (EX x. P(x)) | Q"
-  "!!P Q. |- (EX x. P | Q(x)) <-> P | (EX x. Q(x))"
-  "!!P Q. |- (EX x. P(x) --> Q) <-> (ALL x. P(x)) --> Q"
-  "!!P Q. |- (EX x. P --> Q(x)) <-> P --> (EX x. Q(x))"
+  "\<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) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
+  "\<And>P Q. |- (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
+  "\<And>P Q. |- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+  "\<And>P Q. |- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<exists>x. Q(x))"
   by (fast add!: subst)+
 
 text \<open>universal miniscoping\<close>
 lemma all_simps:
-  "!!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) <-> (EX 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))"
+  "\<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) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<longrightarrow> Q"
+  "\<And>P Q. |- (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<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 (fast add!: subst)+
 
 text \<open>These are NOT supplied by default!\<close>
 lemma distrib_simps:
-  "|- P & (Q | R) <-> P&Q | P&R"
-  "|- (Q | R) & P <-> Q&P | R&P"
-  "|- (P | Q --> R) <-> (P --> R) & (Q --> R)"
+  "|- P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R"
+  "|- (Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P"
+  "|- (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
   by (fast add!: subst)+
 
-lemma P_iff_F: "|- ~P ==> |- (P <-> False)"
+lemma P_iff_F: "|- \<not> P \<Longrightarrow> |- (P \<longleftrightarrow> False)"
   apply (erule thinR [THEN cut])
   apply fast
   done
 
 lemmas iff_reflection_F = P_iff_F [THEN iff_reflection]
 
-lemma P_iff_T: "|- P ==> |- (P <-> True)"
+lemma P_iff_T: "|- P \<Longrightarrow> |- (P \<longleftrightarrow> True)"
   apply (erule thinR [THEN cut])
   apply fast
   done
@@ -130,51 +130,51 @@
 
 
 lemma LK_extra_simps:
-  "|- P | ~P"
-  "|- ~P | P"
-  "|- ~ ~ P <-> P"
-  "|- (~P --> P) <-> P"
-  "|- (~P <-> ~Q) <-> (P<->Q)"
+  "|- P \<or> \<not> P"
+  "|- \<not> P \<or> P"
+  "|- \<not> \<not> P \<longleftrightarrow> P"
+  "|- (\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
+  "|- (\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)"
   by (fast add!: subst)+
 
 
 subsection \<open>Named rewrite rules\<close>
 
-lemma conj_commute: "|- P&Q <-> Q&P"
-  and conj_left_commute: "|- P&(Q&R) <-> Q&(P&R)"
+lemma conj_commute: "|- P \<and> Q \<longleftrightarrow> Q \<and> P"
+  and conj_left_commute: "|- P \<and> (Q \<and> R) \<longleftrightarrow> Q \<and> (P \<and> R)"
   by (fast add!: subst)+
 
 lemmas conj_comms = conj_commute conj_left_commute
 
-lemma disj_commute: "|- P|Q <-> Q|P"
-  and disj_left_commute: "|- P|(Q|R) <-> Q|(P|R)"
+lemma disj_commute: "|- P \<or> Q \<longleftrightarrow> Q \<or> P"
+  and disj_left_commute: "|- P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)"
   by (fast add!: subst)+
 
 lemmas disj_comms = disj_commute disj_left_commute
 
-lemma conj_disj_distribL: "|- P&(Q|R) <-> (P&Q | P&R)"
-  and conj_disj_distribR: "|- (P|Q)&R <-> (P&R | Q&R)"
+lemma conj_disj_distribL: "|- P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)"
+  and conj_disj_distribR: "|- (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> R)"
 
-  and disj_conj_distribL: "|- P|(Q&R) <-> (P|Q) & (P|R)"
-  and disj_conj_distribR: "|- (P&Q)|R <-> (P|R) & (Q|R)"
+  and disj_conj_distribL: "|- P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+  and disj_conj_distribR: "|- (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
 
-  and imp_conj_distrib: "|- (P --> (Q&R)) <-> (P-->Q) & (P-->R)"
-  and imp_conj: "|- ((P&Q)-->R)   <-> (P --> (Q --> R))"
-  and imp_disj: "|- (P|Q --> R)   <-> (P-->R) & (Q-->R)"
+  and imp_conj_distrib: "|- (P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
+  and imp_conj: "|- ((P \<and> Q) \<longrightarrow> R)  \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
+  and imp_disj: "|- (P \<or> Q \<longrightarrow> R)  \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
 
-  and imp_disj1: "|- (P-->Q) | R <-> (P-->Q | R)"
-  and imp_disj2: "|- Q | (P-->R) <-> (P-->Q | R)"
+  and imp_disj1: "|- (P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
+  and imp_disj2: "|- Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
 
-  and de_Morgan_disj: "|- (~(P | Q)) <-> (~P & ~Q)"
-  and de_Morgan_conj: "|- (~(P & Q)) <-> (~P | ~Q)"
+  and de_Morgan_disj: "|- (\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)"
+  and de_Morgan_conj: "|- (\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)"
 
-  and not_iff: "|- ~(P <-> Q) <-> (P <-> ~Q)"
+  and not_iff: "|- \<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)"
   by (fast add!: subst)+
 
 lemma imp_cong:
-  assumes p1: "|- P <-> P'"
-    and p2: "|- P' ==> |- Q <-> Q'"
-  shows "|- (P-->Q) <-> (P'-->Q')"
+  assumes p1: "|- P \<longleftrightarrow> P'"
+    and p2: "|- P' \<Longrightarrow> |- Q \<longleftrightarrow> Q'"
+  shows "|- (P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')"
   apply (lem p1)
   apply safe
    apply (tactic \<open>
@@ -185,9 +185,9 @@
   done
 
 lemma conj_cong:
-  assumes p1: "|- P <-> P'"
-    and p2: "|- P' ==> |- Q <-> Q'"
-  shows "|- (P&Q) <-> (P'&Q')"
+  assumes p1: "|- P \<longleftrightarrow> P'"
+    and p2: "|- P' \<Longrightarrow> |- Q \<longleftrightarrow> Q'"
+  shows "|- (P \<and> Q) \<longleftrightarrow> (P' \<and> Q')"
   apply (lem p1)
   apply safe
    apply (tactic \<open>
@@ -197,7 +197,7 @@
            Cla.safe_tac @{context} 1)\<close>)
   done
 
-lemma eq_sym_conv: "|- (x=y) <-> (y=x)"
+lemma eq_sym_conv: "|- x = y \<longleftrightarrow> y = x"
   by (fast add!: subst)
 
 ML_file "simpdata.ML"
@@ -207,14 +207,14 @@
 
 text \<open>To create substition rules\<close>
 
-lemma eq_imp_subst: "|- a=b ==> $H, A(a), $G |- $E, A(b), $F"
+lemma eq_imp_subst: "|- a = b \<Longrightarrow> $H, A(a), $G |- $E, A(b), $F"
   by simp
 
-lemma split_if: "|- P(if Q then x else y) <-> ((Q --> P(x)) & (~Q --> P(y)))"
+lemma split_if: "|- P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) \<and> (\<not> Q \<longrightarrow> P(y)))"
   apply (rule_tac P = Q in cut)
    prefer 2
    apply (simp add: if_P)
-  apply (rule_tac P = "~Q" in cut)
+  apply (rule_tac P = "\<not> Q" in cut)
    prefer 2
    apply (simp add: if_not_P)
   apply fast
@@ -225,7 +225,7 @@
   apply fast
   done
 
-lemma if_eq_cancel: "|- (if x=y then y else x) = x"
+lemma if_eq_cancel: "|- (if x = y then y else x) = x"
   apply (lem split_if)
   apply safe
   apply (rule symL)
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/LK/Hard_Quantifiers.thy
--- a/src/Sequents/LK/Hard_Quantifiers.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK/Hard_Quantifiers.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -15,251 +15,251 @@
 imports "../LK"
 begin
 
-lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x))  &  (ALL x. Q(x))"
+lemma "|- (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
   by fast
 
-lemma "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
+lemma "|- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
   by fast
 
-lemma "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
+lemma "|- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
   by fast
 
-lemma "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
+lemma "|- (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
   by fast
 
 
 text "Problems requiring quantifier duplication"
 
-(*Not provable by fast: needs multiple instantiation of ALL*)
-lemma "|- (ALL x. P(x)-->P(f(x)))  &  P(d)-->P(f(f(f(d))))"
+(*Not provable by fast: needs multiple instantiation of \<forall>*)
+lemma "|- (\<forall>x. P(x) \<longrightarrow> P(f(x))) \<and> P(d) \<longrightarrow> P(f(f(f(d))))"
   by best_dup
 
 (*Needs double instantiation of the quantifier*)
-lemma "|- EX x. P(x) --> P(a) & P(b)"
+lemma "|- \<exists>x. P(x) \<longrightarrow> P(a) \<and> P(b)"
   by fast_dup
 
-lemma "|- EX z. P(z) --> (ALL x. P(x))"
+lemma "|- \<exists>z. P(z) \<longrightarrow> (\<forall>x. P(x))"
   by best_dup
 
 
 text "Hard examples with quantifiers"
 
 text "Problem 18"
-lemma "|- EX y. ALL x. P(y)-->P(x)"
+lemma "|- \<exists>y. \<forall>x. P(y)\<longrightarrow>P(x)"
   by best_dup
 
 text "Problem 19"
-lemma "|- EX x. ALL y z. (P(y)-->Q(z)) --> (P(x)-->Q(x))"
+lemma "|- \<exists>x. \<forall>y z. (P(y)\<longrightarrow>Q(z)) \<longrightarrow> (P(x)\<longrightarrow>Q(x))"
   by best_dup
 
 text "Problem 20"
-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))"
+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 fast
 
 text "Problem 21"
-lemma "|- (EX x. P-->Q(x)) & (EX x. Q(x)-->P) --> (EX x. P<->Q(x))"
+lemma "|- (\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> (\<exists>x. P \<longleftrightarrow> Q(x))"
   by best_dup
 
 text "Problem 22"
-lemma "|- (ALL x. P <-> Q(x))  -->  (P <-> (ALL x. Q(x)))"
+lemma "|- (\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
   by fast
 
 text "Problem 23"
-lemma "|- (ALL x. P | Q(x))  <->  (P | (ALL x. Q(x)))"
+lemma "|- (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x)))"
   by best
 
 text "Problem 24"
-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))"
+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 pc
 
 text "Problem 25"
-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))"
+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 best
 
 text "Problem 26"
-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)))"
+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 pc
 
 text "Problem 27"
-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))"
+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 pc
 
 text "Problem 28.  AMENDED"
-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))"
+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 pc
 
 text "Problem 29.  Essentially the same as Principia Mathematica *11.71"
-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)))"
+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 pc
 
 text "Problem 30"
-lemma "|- (ALL x. P(x) | Q(x) --> ~ R(x)) &  
-        (ALL x. (Q(x) --> ~ S(x)) --> P(x) & R(x))   
-    --> (ALL x. S(x))"
+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 fast
 
 text "Problem 31"
-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))"
+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 fast
 
 text "Problem 32"
-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))"
+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 best
 
 text "Problem 33"
-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)))"
+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 fast
 
 text "Problem 34  AMENDED (TWICE!!)"
 (*Andrews's challenge*)
-lemma "|- ((EX x. ALL y. p(x) <-> p(y))  <->               
-               ((EX x. q(x)) <-> (ALL y. p(y))))     <->         
-              ((EX x. ALL y. q(x) <-> q(y))  <->                 
-               ((EX x. p(x)) <-> (ALL y. q(y))))"
+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 best_dup
 
 text "Problem 35"
-lemma "|- EX x y. P(x,y) -->  (ALL u v. P(u,v))"
+lemma "|- \<exists>x y. P(x,y) \<longrightarrow> (\<forall>u v. P(u,v))"
   by best_dup
 
 text "Problem 36"
-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))"
+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 fast
 
 text "Problem 37"
-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))"
+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 pc
 
 text "Problem 38"
-lemma "|- (ALL x. p(a) & (p(x) --> (EX y. p(y) & r(x,y))) -->         
-                 (EX z. EX w. p(z) & r(x,w) & r(w,z)))  <->          
-         (ALL x. (~p(a) | p(x) | (EX z. EX w. p(z) & r(x,w) & r(w,z))) &     
-                 (~p(a) | ~(EX y. p(y) & r(x,y)) |                           
-                 (EX z. EX w. p(z) & r(x,w) & r(w,z))))"
+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 pc
 
 text "Problem 39"
-lemma "|- ~ (EX x. ALL y. F(y,x) <-> ~F(y,y))"
+lemma "|- \<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
   by fast
 
 text "Problem 40.  AMENDED"
-lemma "|- (EX y. ALL x. F(x,y) <-> F(x,x)) -->   
-         ~(ALL x. EX y. ALL z. F(z,y) <-> ~ F(z,x))"
+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 fast
 
 text "Problem 41"
-lemma "|- (ALL z. EX y. ALL x. f(x,y) <-> f(x,z) & ~ f(x,x))       
-         --> ~ (EX z. ALL x. f(x,z))"
+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 fast
 
 text "Problem 42"
-lemma "|- ~ (EX y. ALL x. p(x,y) <-> ~ (EX z. p(x,z) & p(z,x)))"
+lemma "|- \<not> (\<exists>y. \<forall>x. p(x,y) \<longleftrightarrow> \<not> (\<exists>z. p(x,z) \<and> p(z,x)))"
   oops
 
 text "Problem 43"
-lemma "|- (ALL x. ALL y. q(x,y) <-> (ALL z. p(z,x) <-> p(z,y)))  
-          --> (ALL x. (ALL y. q(x,y) <-> q(y,x)))"
+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)))"
   oops
 
 text "Problem 44"
-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))"
+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 fast
 
 text "Problem 45"
-lemma "|- (ALL x. f(x) & (ALL y. g(y) & h(x,y) --> j(x,y))         
-                      --> (ALL y. g(y) & h(x,y) --> k(y))) &     
-      ~ (EX y. l(y) & k(y)) &                                    
-      (EX x. f(x) & (ALL y. h(x,y) --> l(y))                     
-                   & (ALL y. g(y) & h(x,y) --> j(x,y)))          
-      --> (EX x. f(x) & ~ (EX y. g(y) & h(x,y)))"
+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 best
 
 
 text "Problems (mainly) involving equality or functions"
 
 text "Problem 48"
-lemma "|- (a=b | c=d) & (a=c | b=d) --> a=d | b=c"
+lemma "|- (a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c"
   by (fast add!: subst)
 
 text "Problem 50"
-lemma "|- (ALL x. P(a,x) | (ALL y. P(x,y))) --> (EX x. ALL y. P(x,y))"
+lemma "|- (\<forall>x. P(a,x) \<or> (\<forall>y. P(x,y))) \<longrightarrow> (\<exists>x. \<forall>y. P(x,y))"
   by best_dup
 
 text "Problem 51"
-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)"
+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 (fast add!: subst)
 
 text "Problem 52"  (*Almost the same as 51. *)
-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)"
+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 (fast add!: subst)
 
 text "Problem 56"
-lemma "|- (ALL x.(EX y. P(y) & x=f(y)) --> P(x)) <-> (ALL x. P(x) --> P(f(x)))"
+lemma "|- (\<forall>x.(\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
   by (best add: symL subst)
   (*requires tricker to orient the equality properly*)
 
 text "Problem 57"
-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))"
+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 fast
 
 text "Problem 58!"
-lemma "|- (ALL x y. f(x)=g(y)) --> (ALL x y. f(f(x))=f(g(y)))"
+lemma "|- (\<forall>x y. f(x) = g(y)) \<longrightarrow> (\<forall>x y. f(f(x)) = f(g(y)))"
   by (fast add!: subst)
 
 text "Problem 59"
 (*Unification works poorly here -- the abstraction %sobj prevents efficient
   operation of the occurs check*)
 
-lemma "|- (ALL x. P(x) <-> ~P(f(x))) --> (EX x. P(x) & ~P(f(x)))"
+lemma "|- (\<forall>x. P(x) \<longleftrightarrow> \<not> P(f(x))) \<longrightarrow> (\<exists>x. P(x) \<and> \<not> P(f(x)))"
   by best_dup
 
 text "Problem 60"
-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))"
   by fast
 
 text "Problem 62 as corrected in JAR 18 (1997), page 135"
-lemma "|- (ALL x. p(a) & (p(x) --> p(f(x))) --> p(f(f(x))))  <->
-      (ALL x. (~p(a) | p(x) | p(f(f(x)))) &                       
-              (~p(a) | ~p(f(x)) | p(f(f(x)))))"
+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 fast
 
 (*18 June 92: loaded in 372 secs*)
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK/Nat.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -14,19 +14,19 @@
 
 axiomatization
   Zero :: nat      ("0") and
-  Suc :: "nat=>nat" and
-  rec :: "[nat, 'a, [nat,'a]=>'a] => 'a"
+  Suc :: "nat \<Rightarrow> nat" and
+  rec :: "[nat, 'a, [nat,'a] \<Rightarrow> 'a] \<Rightarrow> 'a"
 where
-  induct:  "[| $H |- $E, P(0), $F;
-              !!x. $H, P(x) |- $E, P(Suc(x)), $F |] ==> $H |- $E, P(n), $F" and
+  induct:  "\<lbrakk>$H |- $E, P(0), $F;
+             \<And>x. $H, P(x) |- $E, P(Suc(x)), $F\<rbrakk> \<Longrightarrow> $H |- $E, P(n), $F" and
 
-  Suc_inject:  "|- Suc(m)=Suc(n) --> m=n" and
-  Suc_neq_0:   "|- Suc(m) ~= 0" and
+  Suc_inject:  "|- Suc(m) = Suc(n) \<longrightarrow> m = n" and
+  Suc_neq_0:   "|- Suc(m) \<noteq> 0" and
   rec_0:       "|- rec(0,a,f) = a" and
   rec_Suc:     "|- rec(Suc(m), a, f) = f(m, rec(m,a,f))"
 
-definition add :: "[nat, nat] => nat"  (infixl "+" 60)
-  where "m + n == rec(m, n, %x y. Suc(y))"
+definition add :: "[nat, nat] \<Rightarrow> nat"  (infixl "+" 60)
+  where "m + n == rec(m, n, \<lambda>x y. Suc(y))"
 
 
 declare Suc_neq_0 [simp]
@@ -34,40 +34,40 @@
 lemma Suc_inject_rule: "$H, $G, m = n |- $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G |- $E"
   by (rule L_of_imp [OF Suc_inject])
 
-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 simp
   apply (fast add!: Suc_inject_rule)
   done
 
-lemma add_0: "|- 0+n = n"
+lemma add_0: "|- 0 + n = n"
   apply (unfold add_def)
   apply (rule rec_0)
   done
 
-lemma add_Suc: "|- Suc(m)+n = Suc(m+n)"
+lemma add_Suc: "|- Suc(m) + n = Suc(m + n)"
   apply (unfold add_def)
   apply (rule rec_Suc)
   done
 
 declare add_0 [simp] add_Suc [simp]
 
-lemma add_assoc: "|- (k+m)+n = k+(m+n)"
+lemma add_assoc: "|- (k + m) + n = k + (m + n)"
   apply (rule_tac n = "k" in induct)
   apply simp_all
   done
 
-lemma add_0_right: "|- m+0 = m"
+lemma add_0_right: "|- m + 0 = m"
   apply (rule_tac n = "m" in induct)
   apply simp_all
   done
 
-lemma add_Suc_right: "|- m+Suc(n) = Suc(m+n)"
+lemma add_Suc_right: "|- m + Suc(n) = Suc(m + n)"
   apply (rule_tac n = "m" in induct)
   apply simp_all
   done
 
-lemma "(!!n. |- f(Suc(n)) = Suc(f(n))) ==> |- f(i+j) = i+f(j)"
+lemma "(\<And>n. |- f(Suc(n)) = Suc(f(n))) \<Longrightarrow> |- f(i + j) = i + f(j)"
   apply (rule_tac n = "i" in induct)
   apply simp_all
   done
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/LK/Propositional.thy
--- a/src/Sequents/LK/Propositional.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK/Propositional.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -9,75 +9,75 @@
 imports "../LK"
 begin
 
-text "absorptive laws of & and | "
+text "absorptive laws of \<and> and \<or>"
 
-lemma "|- P & P <-> P"
+lemma "|- P \<and> P \<longleftrightarrow> P"
   by fast_prop
 
-lemma "|- P | P <-> P"
+lemma "|- P \<or> P \<longleftrightarrow> P"
   by fast_prop
 
 
-text "commutative laws of & and | "
+text "commutative laws of \<and> and \<or>"
 
-lemma "|- P & Q  <->  Q & P"
+lemma "|- P \<and> Q \<longleftrightarrow> Q \<and> P"
   by fast_prop
 
-lemma "|- P | Q  <->  Q | P"
+lemma "|- P \<or> Q \<longleftrightarrow> Q \<or> P"
   by fast_prop
 
 
-text "associative laws of & and | "
+text "associative laws of \<and> and \<or>"
 
-lemma "|- (P & Q) & R  <->  P & (Q & R)"
+lemma "|- (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
   by fast_prop
 
-lemma "|- (P | Q) | R  <->  P | (Q | R)"
+lemma "|- (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
   by fast_prop
 
 
-text "distributive laws of & and | "
+text "distributive laws of \<and> and \<or>"
 
-lemma "|- (P & Q) | R  <-> (P | R) & (Q | R)"
+lemma "|- (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
   by fast_prop
 
-lemma "|- (P | Q) & R  <-> (P & R) | (Q & R)"
+lemma "|- (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R) \<or> (Q \<and> R)"
   by fast_prop
 
 
 text "Laws involving implication"
 
-lemma "|- (P|Q --> R) <-> (P-->R) & (Q-->R)"
+lemma "|- (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
   by fast_prop
 
-lemma "|- (P & Q --> R) <-> (P--> (Q-->R))"
+lemma "|- (P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
   by fast_prop
 
-lemma "|- (P --> Q & R) <-> (P-->Q)  &  (P-->R)"
+lemma "|- (P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
   by fast_prop
 
 
 text "Classical theorems"
 
-lemma "|- P|Q --> P| ~P&Q"
+lemma "|- P \<or> Q \<longrightarrow> P \<or> \<not> P \<and> Q"
   by fast_prop
 
-lemma "|- (P-->Q)&(~P-->R)  -->  (P&Q | R)"
+lemma "|- (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<or> R)"
   by fast_prop
 
-lemma "|- P&Q | ~P&R  <->  (P-->Q)&(~P-->R)"
+lemma "|- P \<and> Q \<or> \<not> P \<and> R \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
   by fast_prop
 
-lemma "|- (P-->Q) | (P-->R)  <->  (P --> Q | R)"
+lemma "|- (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
   by fast_prop
 
 
 (*If and only if*)
 
-lemma "|- (P<->Q) <-> (Q<->P)"
+lemma "|- (P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
   by fast_prop
 
-lemma "|- ~ (P <-> ~P)"
+lemma "|- \<not> (P \<longleftrightarrow> \<not> P)"
   by fast_prop
 
 
@@ -89,71 +89,71 @@
 *)
 
 (*1*)
-lemma "|- (P-->Q)  <->  (~Q --> ~P)"
+lemma "|- (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
   by fast_prop
 
 (*2*)
-lemma "|- ~ ~ P  <->  P"
+lemma "|- \<not> \<not> P \<longleftrightarrow> P"
   by fast_prop
 
 (*3*)
-lemma "|- ~(P-->Q) --> (Q-->P)"
+lemma "|- \<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
   by fast_prop
 
 (*4*)
-lemma "|- (~P-->Q)  <->  (~Q --> P)"
+lemma "|- (\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
   by fast_prop
 
 (*5*)
-lemma "|- ((P|Q)-->(P|R)) --> (P|(Q-->R))"
+lemma "|- ((P \<or> Q) \<longrightarrow> (P \<or> R)) \<longrightarrow> (P \<or> (Q \<longrightarrow> R))"
   by fast_prop
 
 (*6*)
-lemma "|- P | ~ P"
+lemma "|- P \<or> \<not> P"
   by fast_prop
 
 (*7*)
-lemma "|- P | ~ ~ ~ P"
+lemma "|- P \<or> \<not> \<not> \<not> P"
   by fast_prop
 
 (*8.  Peirce's law*)
-lemma "|- ((P-->Q) --> P)  -->  P"
+lemma "|- ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
   by fast_prop
 
 (*9*)
-lemma "|- ((P|Q) & (~P|Q) & (P| ~Q)) --> ~ (~P | ~Q)"
+lemma "|- ((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)"
   by fast_prop
 
 (*10*)
-lemma "Q-->R, R-->P&Q, P-->(Q|R) |- P<->Q"
+lemma "Q \<longrightarrow> R, R \<longrightarrow> P \<and> Q, P \<longrightarrow> (Q \<or> R) |- P \<longleftrightarrow> Q"
   by fast_prop
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-lemma "|- P<->P"
+lemma "|- P \<longleftrightarrow> P"
   by fast_prop
 
 (*12.  "Dijkstra's law"*)
-lemma "|- ((P <-> Q) <-> R)  <->  (P <-> (Q <-> R))"
+lemma "|- ((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
   by fast_prop
 
 (*13.  Distributive law*)
-lemma "|- P | (Q & R)  <-> (P | Q) & (P | R)"
+lemma "|- P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
   by fast_prop
 
 (*14*)
-lemma "|- (P <-> Q) <-> ((Q | ~P) & (~Q|P))"
+lemma "|- (P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P))"
   by fast_prop
 
 (*15*)
-lemma "|- (P --> Q) <-> (~P | Q)"
+lemma "|- (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
   by fast_prop
 
 (*16*)
-lemma "|- (P-->Q) | (Q-->P)"
+lemma "|- (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"
   by fast_prop
 
 (*17*)
-lemma "|- ((P & (Q-->R))-->S) <-> ((~P | Q | S) & (~P | ~R | S))"
+lemma "|- ((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S))"
   by fast_prop
 
 end
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/LK/Quantifiers.thy
--- a/src/Sequents/LK/Quantifiers.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK/Quantifiers.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -9,94 +9,94 @@
 imports "../LK"
 begin
 
-lemma "|- (ALL x. P)  <->  P"
+lemma "|- (\<forall>x. P) \<longleftrightarrow> P"
   by fast
 
-lemma "|- (ALL x y. P(x,y))  <->  (ALL y x. P(x,y))"
+lemma "|- (\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
   by fast
 
-lemma "ALL u. P(u), ALL v. Q(v) |- ALL u v. P(u) & Q(v)"
+lemma "\<forall>u. P(u), \<forall>v. Q(v) |- \<forall>u v. P(u) \<and> Q(v)"
   by fast
 
 
 text "Permutation of existential quantifier."
 
-lemma "|- (EX x y. P(x,y)) <-> (EX y x. P(x,y))"
+lemma "|- (\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
   by fast
 
-lemma "|- (ALL x. P(x) & Q(x)) <-> (ALL x. P(x)) & (ALL x. Q(x))"
+lemma "|- (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
   by fast
 
 (*Converse is invalid*)
-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 fast
 
 
-text "Pushing ALL into an implication."
+text "Pushing \<forall>into an implication."
 
-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
 
-lemma "|- (EX x. P)  <->  P"
+lemma "|- (\<exists>x. P)  \<longleftrightarrow>  P"
   by fast
 
 
-text "Distribution of EX over disjunction."
+text "Distribution of \<exists>over disjunction."
 
-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
 
 (*Converse is invalid*)
-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 fast
 
 
 text "Harder examples: classical theorems."
 
-lemma "|- (EX x. P-->Q(x))  <->  (P --> (EX x. Q(x)))"
+lemma "|- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
   by fast
 
-lemma "|- (EX x. P(x)-->Q)  <->  (ALL x. P(x)) --> Q"
+lemma "|- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
   by fast
 
-lemma "|- (ALL x. P(x)) | Q  <->  (ALL x. P(x) | Q)"
+lemma "|- (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
   by fast
 
 
 text "Basic test of quantifier reasoning"
 
-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 "The following are invalid!"
 
 (*INVALID*)
-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?
   apply (rule _)
   oops
 
 (*INVALID*)
-lemma "|- (EX x. Q(x))  -->  (ALL x. Q(x))"
+lemma "|- (\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
   apply fast?
   apply (rule _)
   oops
 
 (*INVALID*)
-schematic_goal "|- P(?a) --> (ALL x. P(x))"
+schematic_goal "|- P(?a) \<longrightarrow> (\<forall>x. P(x))"
   apply fast?
   apply (rule _)
   oops
 
 (*INVALID*)
-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?
   apply (rule _)
   oops
@@ -104,35 +104,35 @@
 
 text "Back to things that are provable..."
 
-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
 
 (*An example of why exR should be delayed as long as possible*)
-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 fast
 
 
 text "Solving for a Var"
 
-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
 
 
 text "Principia Mathematica *11.53"
 
-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 fast
 
 
 text "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
 
 
 text "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
 
 
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/LK0.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -21,15 +21,15 @@
 
   True         :: o
   False        :: o
-  equal        :: "['a,'a] => o"     (infixl "=" 50)
-  Not          :: "o => o"           ("~ _" [40] 40)
-  conj         :: "[o,o] => o"       (infixr "&" 35)
-  disj         :: "[o,o] => o"       (infixr "|" 30)
-  imp          :: "[o,o] => o"       (infixr "-->" 25)
-  iff          :: "[o,o] => o"       (infixr "<->" 25)
-  The          :: "('a => o) => 'a"  (binder "THE " 10)
-  All          :: "('a => o) => o"   (binder "ALL " 10)
-  Ex           :: "('a => o) => o"   (binder "EX " 10)
+  equal        :: "['a,'a] \<Rightarrow> o"     (infixl "=" 50)
+  Not          :: "o \<Rightarrow> o"           ("\<not> _" [40] 40)
+  conj         :: "[o,o] \<Rightarrow> o"       (infixr "\<and>" 35)
+  disj         :: "[o,o] \<Rightarrow> o"       (infixr "\<or>" 30)
+  imp          :: "[o,o] \<Rightarrow> o"       (infixr "\<longrightarrow>" 25)
+  iff          :: "[o,o] \<Rightarrow> o"       (infixr "\<longleftrightarrow>" 25)
+  The          :: "('a \<Rightarrow> o) \<Rightarrow> 'a"  (binder "THE " 10)
+  All          :: "('a \<Rightarrow> o) \<Rightarrow> o"   (binder "\<forall>" 10)
+  Ex           :: "('a \<Rightarrow> o) \<Rightarrow> o"   (binder "\<exists>" 10)
 
 syntax
  "_Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
@@ -38,108 +38,98 @@
 print_translation \<open>[(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))]\<close>
 
 abbreviation
-  not_equal  (infixl "~=" 50) where
-  "x ~= y == ~ (x = y)"
-
-notation (xsymbols)
-  Not  ("\<not> _" [40] 40) and
-  conj  (infixr "\<and>" 35) and
-  disj  (infixr "\<or>" 30) and
-  imp  (infixr "\<longrightarrow>" 25) and
-  iff  (infixr "\<longleftrightarrow>" 25) and
-  All  (binder "\<forall>" 10) and
-  Ex  (binder "\<exists>" 10) and
-  not_equal  (infixl "\<noteq>" 50)
+  not_equal  (infixl "\<noteq>" 50) where
+  "x \<noteq> y \<equiv> \<not> (x = y)"
 
 axiomatization where
 
   (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
 
-  contRS: "$H |- $E, $S, $S, $F ==> $H |- $E, $S, $F" and
-  contLS: "$H, $S, $S, $G |- $E ==> $H, $S, $G |- $E" and
+  contRS: "$H |- $E, $S, $S, $F \<Longrightarrow> $H |- $E, $S, $F" and
+  contLS: "$H, $S, $S, $G |- $E \<Longrightarrow> $H, $S, $G |- $E" and
 
-  thinRS: "$H |- $E, $F ==> $H |- $E, $S, $F" and
-  thinLS: "$H, $G |- $E ==> $H, $S, $G |- $E" and
+  thinRS: "$H |- $E, $F \<Longrightarrow> $H |- $E, $S, $F" and
+  thinLS: "$H, $G |- $E \<Longrightarrow> $H, $S, $G |- $E" and
 
-  exchRS: "$H |- $E, $R, $S, $F ==> $H |- $E, $S, $R, $F" and
-  exchLS: "$H, $R, $S, $G |- $E ==> $H, $S, $R, $G |- $E" and
+  exchRS: "$H |- $E, $R, $S, $F \<Longrightarrow> $H |- $E, $S, $R, $F" and
+  exchLS: "$H, $R, $S, $G |- $E \<Longrightarrow> $H, $S, $R, $G |- $E" and
 
-  cut:   "[| $H |- $E, P;  $H, P |- $E |] ==> $H |- $E" and
+  cut:   "\<lbrakk>$H |- $E, P;  $H, P |- $E\<rbrakk> \<Longrightarrow> $H |- $E" and
 
   (*Propositional rules*)
 
   basic: "$H, P, $G |- $E, P, $F" and
 
-  conjR: "[| $H|- $E, P, $F;  $H|- $E, Q, $F |] ==> $H|- $E, P&Q, $F" and
-  conjL: "$H, P, Q, $G |- $E ==> $H, P & Q, $G |- $E" and
+  conjR: "\<lbrakk>$H|- $E, P, $F;  $H|- $E, Q, $F\<rbrakk> \<Longrightarrow> $H|- $E, P \<and> Q, $F" and
+  conjL: "$H, P, Q, $G |- $E \<Longrightarrow> $H, P \<and> Q, $G |- $E" and
 
-  disjR: "$H |- $E, P, Q, $F ==> $H |- $E, P|Q, $F" and
-  disjL: "[| $H, P, $G |- $E;  $H, Q, $G |- $E |] ==> $H, P|Q, $G |- $E" and
+  disjR: "$H |- $E, P, Q, $F \<Longrightarrow> $H |- $E, P \<or> Q, $F" and
+  disjL: "\<lbrakk>$H, P, $G |- $E;  $H, Q, $G |- $E\<rbrakk> \<Longrightarrow> $H, P \<or> Q, $G |- $E" and
 
-  impR:  "$H, P |- $E, Q, $F ==> $H |- $E, P-->Q, $F" and
-  impL:  "[| $H,$G |- $E,P;  $H, Q, $G |- $E |] ==> $H, P-->Q, $G |- $E" and
+  impR:  "$H, P |- $E, Q, $F \<Longrightarrow> $H |- $E, P \<longrightarrow> Q, $F" and
+  impL:  "\<lbrakk>$H,$G |- $E,P;  $H, Q, $G |- $E\<rbrakk> \<Longrightarrow> $H, P \<longrightarrow> Q, $G |- $E" and
 
-  notR:  "$H, P |- $E, $F ==> $H |- $E, ~P, $F" and
-  notL:  "$H, $G |- $E, P ==> $H, ~P, $G |- $E" and
+  notR:  "$H, P |- $E, $F \<Longrightarrow> $H |- $E, \<not> P, $F" and
+  notL:  "$H, $G |- $E, P \<Longrightarrow> $H, \<not> P, $G |- $E" and
 
   FalseL: "$H, False, $G |- $E" and
 
-  True_def: "True == False-->False" and
-  iff_def:  "P<->Q == (P-->Q) & (Q-->P)"
+  True_def: "True \<equiv> False \<longrightarrow> False" and
+  iff_def:  "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
 
 axiomatization where
   (*Quantifiers*)
 
-  allR:  "(!!x.$H |- $E, P(x), $F) ==> $H |- $E, ALL x. P(x), $F" and
-  allL:  "$H, P(x), $G, ALL x. P(x) |- $E ==> $H, ALL x. P(x), $G |- $E" and
+  allR:  "(\<And>x. $H |- $E, P(x), $F) \<Longrightarrow> $H |- $E, \<forall>x. P(x), $F" and
+  allL:  "$H, P(x), $G, \<forall>x. P(x) |- $E \<Longrightarrow> $H, \<forall>x. P(x), $G |- $E" and
 
-  exR:   "$H |- $E, P(x), $F, EX x. P(x) ==> $H |- $E, EX x. P(x), $F" and
-  exL:   "(!!x.$H, P(x), $G |- $E) ==> $H, EX x. P(x), $G |- $E" and
+  exR:   "$H |- $E, P(x), $F, \<exists>x. P(x) \<Longrightarrow> $H |- $E, \<exists>x. P(x), $F" and
+  exL:   "(\<And>x. $H, P(x), $G |- $E) \<Longrightarrow> $H, \<exists>x. P(x), $G |- $E" and
 
   (*Equality*)
-  refl:  "$H |- $E, a=a, $F" and
-  subst: "\<And>G H E. $H(a), $G(a) |- $E(a) ==> $H(b), a=b, $G(b) |- $E(b)"
+  refl:  "$H |- $E, a = a, $F" and
+  subst: "\<And>G H E. $H(a), $G(a) |- $E(a) \<Longrightarrow> $H(b), a=b, $G(b) |- $E(b)"
 
   (* Reflection *)
 
 axiomatization where
-  eq_reflection:  "|- x=y ==> (x==y)" and
-  iff_reflection: "|- P<->Q ==> (P==Q)"
+  eq_reflection:  "|- x = y \<Longrightarrow> (x \<equiv> y)" and
+  iff_reflection: "|- P \<longleftrightarrow> Q \<Longrightarrow> (P \<equiv> Q)"
 
   (*Descriptions*)
 
 axiomatization where
-  The: "[| $H |- $E, P(a), $F;  !!x.$H, P(x) |- $E, x=a, $F |] ==>
-          $H |- $E, P(THE x. P(x)), $F"
+  The: "\<lbrakk>$H |- $E, P(a), $F;  \<And>x.$H, P(x) |- $E, x=a, $F\<rbrakk> \<Longrightarrow>
+         $H |- $E, P(THE x. P(x)), $F"
 
-definition If :: "[o, 'a, 'a] => 'a" ("(if (_)/ then (_)/ else (_))" 10)
-  where "If(P,x,y) == THE z::'a. (P --> z=x) & (~P --> z=y)"
+definition If :: "[o, 'a, 'a] \<Rightarrow> 'a" ("(if (_)/ then (_)/ else (_))" 10)
+  where "If(P,x,y) \<equiv> THE z::'a. (P \<longrightarrow> z = x) \<and> (\<not> P \<longrightarrow> z = y)"
 
 
 (** Structural Rules on formulas **)
 
 (*contraction*)
 
-lemma contR: "$H |- $E, P, P, $F ==> $H |- $E, P, $F"
+lemma contR: "$H |- $E, P, P, $F \<Longrightarrow> $H |- $E, P, $F"
   by (rule contRS)
 
-lemma contL: "$H, P, P, $G |- $E ==> $H, P, $G |- $E"
+lemma contL: "$H, P, P, $G |- $E \<Longrightarrow> $H, P, $G |- $E"
   by (rule contLS)
 
 (*thinning*)
 
-lemma thinR: "$H |- $E, $F ==> $H |- $E, P, $F"
+lemma thinR: "$H |- $E, $F \<Longrightarrow> $H |- $E, P, $F"
   by (rule thinRS)
 
-lemma thinL: "$H, $G |- $E ==> $H, P, $G |- $E"
+lemma thinL: "$H, $G |- $E \<Longrightarrow> $H, P, $G |- $E"
   by (rule thinLS)
 
 (*exchange*)
 
-lemma exchR: "$H |- $E, Q, P, $F ==> $H |- $E, P, Q, $F"
+lemma exchR: "$H |- $E, Q, P, $F \<Longrightarrow> $H |- $E, P, Q, $F"
   by (rule exchRS)
 
-lemma exchL: "$H, Q, P, $G |- $E ==> $H, P, Q, $G |- $E"
+lemma exchL: "$H, Q, P, $G |- $E \<Longrightarrow> $H, P, Q, $G |- $E"
   by (rule exchLS)
 
 ML \<open>
@@ -156,19 +146,17 @@
 
 
 (** If-and-only-if rules **)
-lemma iffR:
-    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
+lemma iffR: "\<lbrakk>$H,P |- $E,Q,$F;  $H,Q |- $E,P,$F\<rbrakk> \<Longrightarrow> $H |- $E, P \<longleftrightarrow> Q, $F"
   apply (unfold iff_def)
   apply (assumption | rule conjR impR)+
   done
 
-lemma iffL:
-    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
+lemma iffL: "\<lbrakk>$H,$G |- $E,P,Q;  $H,Q,P,$G |- $E\<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G |- $E"
   apply (unfold iff_def)
   apply (assumption | rule conjL impL basic)+
   done
 
-lemma iff_refl: "$H |- $E, (P <-> P), $F"
+lemma iff_refl: "$H |- $E, (P \<longleftrightarrow> P), $F"
   apply (rule iffR basic)+
   done
 
@@ -181,7 +169,7 @@
 (*Descriptions*)
 lemma the_equality:
   assumes p1: "$H |- $E, P(a), $F"
-    and p2: "!!x. $H, P(x) |- $E, x=a, $F"
+    and p2: "\<And>x. $H, P(x) |- $E, x=a, $F"
   shows "$H |- $E, (THE x. P(x)) = a, $F"
   apply (rule cut)
    apply (rule_tac [2] p2)
@@ -192,12 +180,12 @@
 
 (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
 
-lemma allL_thin: "$H, P(x), $G |- $E ==> $H, ALL x. P(x), $G |- $E"
+lemma allL_thin: "$H, P(x), $G |- $E \<Longrightarrow> $H, \<forall>x. P(x), $G |- $E"
   apply (rule allL)
   apply (erule thinL)
   done
 
-lemma exR_thin: "$H |- $E, P(x), $F ==> $H |- $E, EX x. P(x), $F"
+lemma exR_thin: "$H |- $E, P(x), $F \<Longrightarrow> $H |- $E, \<exists>x. P(x), $F"
   apply (rule exR)
   apply (erule thinR)
   done
@@ -245,7 +233,7 @@
 
 
 lemma mp_R:
-  assumes major: "$H |- $E, $F, P --> Q"
+  assumes major: "$H |- $E, $F, P \<longrightarrow> Q"
     and minor: "$H |- $E, $F, P"
   shows "$H |- $E, Q, $F"
   apply (rule thinRS [THEN cut], rule major)
@@ -254,7 +242,7 @@
   done
 
 lemma mp_L:
-  assumes major: "$H, $G |- $E, P --> Q"
+  assumes major: "$H, $G |- $E, P \<longrightarrow> Q"
     and minor: "$H, $G, Q |- $E"
   shows "$H, P, $G |- $E"
   apply (rule thinL [THEN cut], rule major)
@@ -266,7 +254,7 @@
 (** Two rules to generate left- and right- rules from implications **)
 
 lemma R_of_imp:
-  assumes major: "|- P --> Q"
+  assumes major: "|- P \<longrightarrow> Q"
     and minor: "$H |- $E, $F, P"
   shows "$H |- $E, Q, $F"
   apply (rule mp_R)
@@ -275,7 +263,7 @@
   done
 
 lemma L_of_imp:
-  assumes major: "|- P --> Q"
+  assumes major: "|- P \<longrightarrow> Q"
     and minor: "$H, $G, Q |- $E"
   shows "$H, P, $G |- $E"
   apply (rule mp_L)
@@ -285,24 +273,24 @@
 
 (*Can be used to create implications in a subgoal*)
 lemma backwards_impR:
-  assumes prem: "$H, $G |- $E, $F, P --> Q"
+  assumes prem: "$H, $G |- $E, $F, P \<longrightarrow> Q"
   shows "$H, P, $G |- $E, Q, $F"
   apply (rule mp_L)
    apply (rule_tac [2] basic)
   apply (rule thinR, rule prem)
   done
 
-lemma conjunct1: "|-P&Q ==> |-P"
+lemma conjunct1: "|-P \<and> Q \<Longrightarrow> |-P"
   apply (erule thinR [THEN cut])
   apply fast
   done
 
-lemma conjunct2: "|-P&Q ==> |-Q"
+lemma conjunct2: "|-P \<and> Q \<Longrightarrow> |-Q"
   apply (erule thinR [THEN cut])
   apply fast
   done
 
-lemma spec: "|- (ALL x. P(x)) ==> |- P(x)"
+lemma spec: "|- (\<forall>x. P(x)) \<Longrightarrow> |- P(x)"
   apply (erule thinR [THEN cut])
   apply fast
   done
@@ -310,10 +298,10 @@
 
 (** Equality **)
 
-lemma sym: "|- a=b --> b=a"
+lemma sym: "|- a = b \<longrightarrow> b = a"
   by (safe add!: subst)
 
-lemma trans: "|- a=b --> b=c --> a=c"
+lemma trans: "|- a = b \<longrightarrow> b = c \<longrightarrow> a = c"
   by (safe add!: subst)
 
 (* Symmetry of equality in hypotheses *)
@@ -322,18 +310,18 @@
 (* Symmetry of equality in hypotheses *)
 lemmas symR = sym [THEN R_of_imp]
 
-lemma transR: "[| $H|- $E, $F, a=b;  $H|- $E, $F, b=c |] ==> $H|- $E, a=c, $F"
+lemma transR: "\<lbrakk>$H|- $E, $F, a = b;  $H|- $E, $F, b=c\<rbrakk> \<Longrightarrow> $H|- $E, a = c, $F"
   by (rule trans [THEN R_of_imp, THEN mp_R])
 
 (* Two theorms for rewriting only one instance of a definition:
    the first for definitions of formulae and the second for terms *)
 
-lemma def_imp_iff: "(A == B) ==> |- A <-> B"
+lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> |- A \<longleftrightarrow> B"
   apply unfold
   apply (rule iff_refl)
   done
 
-lemma meta_eq_to_obj_eq: "(A == B) ==> |- A = B"
+lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> |- A = B"
   apply unfold
   apply (rule refl)
   done
@@ -347,13 +335,13 @@
 lemma if_False: "|- (if False then x else y) = y"
   unfolding If_def by fast
 
-lemma if_P: "|- P ==> |- (if P then x else y) = x"
+lemma if_P: "|- P \<Longrightarrow> |- (if P then x else y) = x"
   apply (unfold If_def)
   apply (erule thinR [THEN cut])
   apply fast
   done
 
-lemma if_not_P: "|- ~P ==> |- (if P then x else y) = y"
+lemma if_not_P: "|- \<not> P \<Longrightarrow> |- (if P then x else y) = y"
   apply (unfold If_def)
   apply (erule thinR [THEN cut])
   apply fast
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/Modal0.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -10,10 +10,10 @@
 ML_file "modal.ML"
 
 consts
-  box           :: "o=>o"       ("[]_" [50] 50)
-  dia           :: "o=>o"       ("<>_" [50] 50)
-  strimp        :: "[o,o]=>o"   (infixr "--<" 25)
-  streqv        :: "[o,o]=>o"   (infixr ">-<" 25)
+  box           :: "o\<Rightarrow>o"       ("[]_" [50] 50)
+  dia           :: "o\<Rightarrow>o"       ("<>_" [50] 50)
+  strimp        :: "[o,o]\<Rightarrow>o"   (infixr "--<" 25)
+  streqv        :: "[o,o]\<Rightarrow>o"   (infixr ">-<" 25)
   Lstar         :: "two_seqi"
   Rstar         :: "two_seqi"
 
@@ -37,20 +37,18 @@
 \<close>
 
 defs
-  strimp_def:    "P --< Q == [](P --> Q)"
-  streqv_def:    "P >-< Q == (P --< Q) & (Q --< P)"
+  strimp_def:    "P --< Q == [](P \<longrightarrow> Q)"
+  streqv_def:    "P >-< Q == (P --< Q) \<and> (Q --< P)"
 
 
 lemmas rewrite_rls = strimp_def streqv_def
 
-lemma iffR:
-    "[| $H,P |- $E,Q,$F;  $H,Q |- $E,P,$F |] ==> $H |- $E, P <-> Q, $F"
+lemma iffR: "\<lbrakk>$H,P |- $E,Q,$F;  $H,Q |- $E,P,$F\<rbrakk> \<Longrightarrow> $H |- $E, P \<longleftrightarrow> Q, $F"
   apply (unfold iff_def)
   apply (assumption | rule conjR impR)+
   done
 
-lemma iffL:
-    "[| $H,$G |- $E,P,Q;  $H,Q,P,$G |- $E |] ==> $H, P <-> Q, $G |- $E"
+lemma iffL: "\<lbrakk>$H,$G |- $E,P,Q;  $H,Q,P,$G |- $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G |- $E"
   apply (unfold iff_def)
   apply (assumption | rule conjL impL basic)+
   done
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/S4.thy
--- a/src/Sequents/S4.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/S4.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -13,23 +13,23 @@
 (*                 delta * == {<>P | <>P : delta}               *)
 
   lstar0:         "|L>" and
-  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H" and
-  lstar2:         "$G |L> $H ==>   P, $G |L>      $H" and
+  lstar1:         "$G |L> $H \<Longrightarrow> []P, $G |L> []P, $H" and
+  lstar2:         "$G |L> $H \<Longrightarrow>   P, $G |L>      $H" and
   rstar0:         "|R>" and
-  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H" and
-  rstar2:         "$G |R> $H ==>   P, $G |R>      $H" and
+  rstar1:         "$G |R> $H \<Longrightarrow> <>P, $G |R> <>P, $H" and
+  rstar2:         "$G |R> $H \<Longrightarrow>   P, $G |R>      $H" and
 
 (* Rules for [] and <> *)
 
   boxR:
-   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
-           $E'         |- $F', P, $G'|] ==> $E          |- $F, []P, $G" and
-  boxL:     "$E,P,$F,[]P |-         $G    ==> $E, []P, $F |-          $G" and
+   "\<lbrakk>$E |L> $E';  $F |R> $F';  $G |R> $G';
+           $E'         |- $F', P, $G'\<rbrakk> \<Longrightarrow> $E          |- $F, []P, $G" and
+  boxL:     "$E,P,$F,[]P |-         $G    \<Longrightarrow> $E, []P, $F |-          $G" and
 
-  diaR:     "$E          |- $F,P,$G,<>P   ==> $E          |- $F, <>P, $G" and
+  diaR:     "$E          |- $F,P,$G,<>P   \<Longrightarrow> $E          |- $F, <>P, $G" and
   diaL:
-   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
-           $E', P, $F' |-         $G'|] ==> $E, <>P, $F |- $G"
+   "\<lbrakk>$E |L> $E';  $F |L> $F';  $G |R> $G';
+           $E', P, $F' |-         $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F |- $G"
 
 ML \<open>
 structure S4_Prover = Modal_ProverFun
@@ -49,63 +49,63 @@
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
 
-lemma "|- []P --> P" by S4_solve
-lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S4_solve   (* normality*)
-lemma "|- (P--<Q) --> []P --> []Q" by S4_solve
-lemma "|- P --> <>P" by S4_solve
+lemma "|- []P \<longrightarrow> P" by S4_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S4_solve   (* normality*)
+lemma "|- (P --< Q) \<longrightarrow> []P \<longrightarrow> []Q" by S4_solve
+lemma "|- P \<longrightarrow> <>P" by S4_solve
 
-lemma "|-  [](P & Q) <-> []P & []Q" by S4_solve
-lemma "|-  <>(P | Q) <-> <>P | <>Q" by S4_solve
-lemma "|-  [](P<->Q) <-> (P>-<Q)" by S4_solve
-lemma "|-  <>(P-->Q) <-> ([]P--><>Q)" by S4_solve
-lemma "|-        []P <-> ~<>(~P)" by S4_solve
-lemma "|-     [](~P) <-> ~<>P" by S4_solve
-lemma "|-       ~[]P <-> <>(~P)" by S4_solve
-lemma "|-      [][]P <-> ~<><>(~P)" by S4_solve
-lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S4_solve
+lemma "|-  [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve
+lemma "|-  <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve
+lemma "|-  [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >-< Q)" by S4_solve
+lemma "|-  <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S4_solve
+lemma "|-        []P \<longleftrightarrow> \<not> <>(\<not> P)" by S4_solve
+lemma "|-     [](\<not> P) \<longleftrightarrow> \<not> <>P" by S4_solve
+lemma "|-       \<not> []P \<longleftrightarrow> <>(\<not> P)" by S4_solve
+lemma "|-      [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S4_solve
+lemma "|- \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by S4_solve
 
-lemma "|- []P | []Q --> [](P | Q)" by S4_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S4_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S4_solve
-lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S4_solve
-lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by S4_solve
-lemma "|- []P --> <>Q --> <>(P & Q)" by S4_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve
+lemma "|- <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S4_solve
+lemma "|- (P --< Q) \<and> (Q --< R) \<longrightarrow> (P --< R)" by S4_solve
+lemma "|- []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
 
 
 (* Theorems of system S4 from Hughes and Cresswell, p.46 *)
 
-lemma "|- []A --> A" by S4_solve             (* refexivity *)
-lemma "|- []A --> [][]A" by S4_solve         (* transitivity *)
-lemma "|- []A --> <>A" by S4_solve           (* seriality *)
-lemma "|- <>[](<>A --> []<>A)" by S4_solve
-lemma "|- <>[](<>[]A --> []A)" by S4_solve
-lemma "|- []P <-> [][]P" by S4_solve
-lemma "|- <>P <-> <><>P" by S4_solve
-lemma "|- <>[]<>P --> <>P" by S4_solve
-lemma "|- []<>P <-> []<>[]<>P" by S4_solve
-lemma "|- <>[]P <-> <>[]<>[]P" by S4_solve
+lemma "|- []A \<longrightarrow> A" by S4_solve             (* refexivity *)
+lemma "|- []A \<longrightarrow> [][]A" by S4_solve         (* transitivity *)
+lemma "|- []A \<longrightarrow> <>A" by S4_solve           (* seriality *)
+lemma "|- <>[](<>A \<longrightarrow> []<>A)" by S4_solve
+lemma "|- <>[](<>[]A \<longrightarrow> []A)" by S4_solve
+lemma "|- []P \<longleftrightarrow> [][]P" by S4_solve
+lemma "|- <>P \<longleftrightarrow> <><>P" by S4_solve
+lemma "|- <>[]<>P \<longrightarrow> <>P" by S4_solve
+lemma "|- []<>P \<longleftrightarrow> []<>[]<>P" by S4_solve
+lemma "|- <>[]P \<longleftrightarrow> <>[]<>[]P" by S4_solve
 
 (* Theorems for system S4 from Hughes and Cresswell, p.60 *)
 
-lemma "|- []P | []Q <-> []([]P | []Q)" by S4_solve
-lemma "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)" by S4_solve
+lemma "|- []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S4_solve
+lemma "|- ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S4_solve
 
 (* These are from Hailpern, LNCS 129 *)
 
-lemma "|- [](P & Q) <-> []P & []Q" by S4_solve
-lemma "|- <>(P | Q) <-> <>P | <>Q" by S4_solve
-lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S4_solve
+lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve
+lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve
+lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S4_solve
 
-lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S4_solve
-lemma "|- []P --> []<>P" by S4_solve
-lemma "|- <>[]P --> <>P" by S4_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S4_solve
+lemma "|- []P \<longrightarrow> []<>P" by S4_solve
+lemma "|- <>[]P \<longrightarrow> <>P" by S4_solve
 
-lemma "|- []P | []Q --> [](P | Q)" by S4_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S4_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S4_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S4_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S4_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve
 
 end
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/S43.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -10,10 +10,10 @@
 begin
 
 consts
-  S43pi :: "[seq'=>seq', seq'=>seq', seq'=>seq',
-             seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
+  S43pi :: "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq',
+             seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
 syntax
-  "_S43pi" :: "[seq, seq, seq, seq, seq, seq] => prop"
+  "_S43pi" :: "[seq, seq, seq, seq, seq, seq] \<Rightarrow> prop"
                          ("S43pi((_);(_);(_);(_);(_);(_))" [] 5)
 
 parse_translation \<open>
@@ -38,11 +38,11 @@
 (*                 delta * == {<>P | <>P : delta}                *)
 
   lstar0:         "|L>" and
-  lstar1:         "$G |L> $H ==> []P, $G |L> []P, $H" and
-  lstar2:         "$G |L> $H ==>   P, $G |L>      $H" and
+  lstar1:         "$G |L> $H \<Longrightarrow> []P, $G |L> []P, $H" and
+  lstar2:         "$G |L> $H \<Longrightarrow>   P, $G |L>      $H" and
   rstar0:         "|R>" and
-  rstar1:         "$G |R> $H ==> <>P, $G |R> <>P, $H" and
-  rstar2:         "$G |R> $H ==>   P, $G |R>      $H" and
+  rstar1:         "$G |R> $H \<Longrightarrow> <>P, $G |R> <>P, $H" and
+  rstar2:         "$G |R> $H \<Longrightarrow>   P, $G |R>      $H" and
 
 (* Set of Horn clauses to generate the antecedents for the S43 pi rule       *)
 (* ie                                                                        *)
@@ -56,23 +56,23 @@
 
   S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia" and
   S43pi1:
-   "[| (S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia |] ==>
+   "\<lbrakk>(S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia\<rbrakk> \<Longrightarrow>
        S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia" and
   S43pi2:
-   "[| (S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia |] ==>
+   "\<lbrakk>(S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia\<rbrakk> \<Longrightarrow>
        S43pi $L';;     $R'; []P,$R; $Lbox;$Rdia" and
 
 (* Rules for [] and <> for S43 *)
 
-  boxL:           "$E, P, $F, []P |- $G ==> $E, []P, $F |- $G" and
-  diaR:           "$E |- $F, P, $G, <>P ==> $E |- $F, <>P, $G" and
+  boxL:           "$E, P, $F, []P |- $G \<Longrightarrow> $E, []P, $F |- $G" and
+  diaR:           "$E |- $F, P, $G, <>P \<Longrightarrow> $E |- $F, <>P, $G" and
   pi1:
-   "[| $L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;
-      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
+   "\<lbrakk>$L1,<>P,$L2 |L> $Lbox;  $L1,<>P,$L2 |R> $Ldia;  $R |L> $Rbox;  $R |R> $Rdia;
+      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia\<rbrakk> \<Longrightarrow>
    $L1, <>P, $L2 |- $R" and
   pi2:
-   "[| $L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;
-      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia |] ==>
+   "\<lbrakk>$L |L> $Lbox;  $L |R> $Ldia;  $R1,[]P,$R2 |L> $Rbox;  $R1,[]P,$R2 |R> $Rdia;
+      S43pi ; $Ldia;; $Rbox; $Lbox; $Rdia\<rbrakk> \<Longrightarrow>
    $L |- $R1, []P, $R2"
 
 
@@ -97,108 +97,108 @@
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
 
-lemma "|- []P --> P" by S43_solve
-lemma "|- [](P-->Q) --> ([]P-->[]Q)" by S43_solve   (* normality*)
-lemma "|- (P--<Q) --> []P --> []Q" by S43_solve
-lemma "|- P --> <>P" by S43_solve
+lemma "|- []P \<longrightarrow> P" by S43_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S43_solve   (* normality*)
+lemma "|- (P--<Q) \<longrightarrow> []P \<longrightarrow> []Q" by S43_solve
+lemma "|- P \<longrightarrow> <>P" by S43_solve
 
-lemma "|-  [](P & Q) <-> []P & []Q" by S43_solve
-lemma "|-  <>(P | Q) <-> <>P | <>Q" by S43_solve
-lemma "|-  [](P<->Q) <-> (P>-<Q)" by S43_solve
-lemma "|-  <>(P-->Q) <-> ([]P--><>Q)" by S43_solve
-lemma "|-        []P <-> ~<>(~P)" by S43_solve
-lemma "|-     [](~P) <-> ~<>P" by S43_solve
-lemma "|-       ~[]P <-> <>(~P)" by S43_solve
-lemma "|-      [][]P <-> ~<><>(~P)" by S43_solve
-lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by S43_solve
+lemma "|-  [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "|-  <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "|-  [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P>-<Q)" by S43_solve
+lemma "|-  <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve
+lemma "|-        []P \<longleftrightarrow> \<not> <>(\<not> P)" by S43_solve
+lemma "|-     [](\<not>P) \<longleftrightarrow> \<not> <>P" by S43_solve
+lemma "|-       \<not> []P \<longleftrightarrow> <>(\<not> P)" by S43_solve
+lemma "|-      [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S43_solve
+lemma "|- \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by S43_solve
 
-lemma "|- []P | []Q --> [](P | Q)" by S43_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S43_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S43_solve
-lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by S43_solve
-lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by S43_solve
-lemma "|- []P --> <>Q --> <>(P & Q)" by S43_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
+lemma "|- <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S43_solve
+lemma "|- (P --< Q) \<and> (Q --<R ) \<longrightarrow> (P --< R)" by S43_solve
+lemma "|- []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
 
 
 (* Theorems of system S4 from Hughes and Cresswell, p.46 *)
 
-lemma "|- []A --> A" by S43_solve             (* refexivity *)
-lemma "|- []A --> [][]A" by S43_solve         (* transitivity *)
-lemma "|- []A --> <>A" by S43_solve           (* seriality *)
-lemma "|- <>[](<>A --> []<>A)" by S43_solve
-lemma "|- <>[](<>[]A --> []A)" by S43_solve
-lemma "|- []P <-> [][]P" by S43_solve
-lemma "|- <>P <-> <><>P" by S43_solve
-lemma "|- <>[]<>P --> <>P" by S43_solve
-lemma "|- []<>P <-> []<>[]<>P" by S43_solve
-lemma "|- <>[]P <-> <>[]<>[]P" by S43_solve
+lemma "|- []A \<longrightarrow> A" by S43_solve             (* refexivity *)
+lemma "|- []A \<longrightarrow> [][]A" by S43_solve         (* transitivity *)
+lemma "|- []A \<longrightarrow> <>A" by S43_solve           (* seriality *)
+lemma "|- <>[](<>A \<longrightarrow> []<>A)" by S43_solve
+lemma "|- <>[](<>[]A \<longrightarrow> []A)" by S43_solve
+lemma "|- []P \<longleftrightarrow> [][]P" by S43_solve
+lemma "|- <>P \<longleftrightarrow> <><>P" by S43_solve
+lemma "|- <>[]<>P \<longrightarrow> <>P" by S43_solve
+lemma "|- []<>P \<longleftrightarrow> []<>[]<>P" by S43_solve
+lemma "|- <>[]P \<longleftrightarrow> <>[]<>[]P" by S43_solve
 
 (* Theorems for system S4 from Hughes and Cresswell, p.60 *)
 
-lemma "|- []P | []Q <-> []([]P | []Q)" by S43_solve
-lemma "|- ((P>-<Q) --< R) --> ((P>-<Q) --< []R)" by S43_solve
+lemma "|- []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S43_solve
+lemma "|- ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S43_solve
 
 (* These are from Hailpern, LNCS 129 *)
 
-lemma "|- [](P & Q) <-> []P & []Q" by S43_solve
-lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve
-lemma "|- <>(P --> Q) <-> ([]P --> <>Q)" by S43_solve
+lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve
 
-lemma "|- [](P --> Q) --> (<>P --> <>Q)" by S43_solve
-lemma "|- []P --> []<>P" by S43_solve
-lemma "|- <>[]P --> <>P" by S43_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S43_solve
+lemma "|- []P \<longrightarrow> []<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> <>P" by S43_solve
 
-lemma "|- []P | []Q --> [](P | Q)" by S43_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S43_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S43_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
 
 
 (* Theorems of system S43 *)
 
-lemma "|- <>[]P --> []<>P" by S43_solve
-lemma "|- <>[]P --> [][]<>P" by S43_solve
-lemma "|- [](<>P | <>Q) --> []<>P | []<>Q" by S43_solve
-lemma "|- <>[]P & <>[]Q --> <>([]P & []Q)" by S43_solve
-lemma "|- []([]P --> []Q) | []([]Q --> []P)" by S43_solve
-lemma "|- [](<>P --> <>Q) | [](<>Q --> <>P)" by S43_solve
-lemma "|- []([]P --> Q) | []([]Q --> P)" by S43_solve
-lemma "|- [](P --> <>Q) | [](Q --> <>P)" by S43_solve
-lemma "|- [](P --> []Q-->R) | [](P | ([]R --> Q))" by S43_solve
-lemma "|- [](P | (Q --> <>C)) | [](P --> C --> <>Q)" by S43_solve
-lemma "|- []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve
-lemma "|- <>P & <>Q --> <>(<>P & Q) | <>(P & <>Q)" by S43_solve
-lemma "|- [](P | Q) & []([]P | Q) & [](P | []Q) --> []P | []Q" by S43_solve
-lemma "|- <>P & <>Q --> <>(P & Q) | <>(<>P & Q) | <>(P & <>Q)" by S43_solve
-lemma "|- <>[]<>P <-> []<>P" by S43_solve
-lemma "|- []<>[]P <-> <>[]P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> [][]<>P" by S43_solve
+lemma "|- [](<>P \<or> <>Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
+lemma "|- <>[]P \<and> <>[]Q \<longrightarrow> <>([]P \<and> []Q)" by S43_solve
+lemma "|- []([]P \<longrightarrow> []Q) \<or> []([]Q \<longrightarrow> []P)" by S43_solve
+lemma "|- [](<>P \<longrightarrow> <>Q) \<or> [](<>Q \<longrightarrow> <>P)" by S43_solve
+lemma "|- []([]P \<longrightarrow> Q) \<or> []([]Q \<longrightarrow> P)" by S43_solve
+lemma "|- [](P \<longrightarrow> <>Q) \<or> [](Q \<longrightarrow> <>P)" by S43_solve
+lemma "|- [](P \<longrightarrow> []Q \<longrightarrow> R) \<or> [](P \<or> ([]R \<longrightarrow> Q))" by S43_solve
+lemma "|- [](P \<or> (Q \<longrightarrow> <>C)) \<or> [](P \<longrightarrow> C \<longrightarrow> <>Q)" by S43_solve
+lemma "|- []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
+lemma "|- <>P \<and> <>Q \<longrightarrow> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
+lemma "|- [](P \<or> Q) \<and> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
+lemma "|- <>P \<and> <>Q \<longrightarrow> <>(P \<and> Q) \<or> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
+lemma "|- <>[]<>P \<longleftrightarrow> []<>P" by S43_solve
+lemma "|- []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
 
 (* These are from Hailpern, LNCS 129 *)
 
-lemma "|- [](P & Q) <-> []P & []Q" by S43_solve
-lemma "|- <>(P | Q) <-> <>P | <>Q" by S43_solve
-lemma "|- <>(P --> Q) <-> []P --> <>Q" by S43_solve
+lemma "|- [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "|- <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "|- <>(P \<longrightarrow> Q) \<longleftrightarrow> []P \<longrightarrow> <>Q" by S43_solve
 
-lemma "|- [](P --> Q) --> <>P --> <>Q" by S43_solve
-lemma "|- []P --> []<>P" by S43_solve
-lemma "|- <>[]P --> <>P" by S43_solve
-lemma "|- []<>[]P --> []<>P" by S43_solve
-lemma "|- <>[]P --> <>[]<>P" by S43_solve
-lemma "|- <>[]P --> []<>P" by S43_solve
-lemma "|- []<>[]P <-> <>[]P" by S43_solve
-lemma "|- <>[]<>P <-> []<>P" by S43_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> <>P \<longrightarrow> <>Q" by S43_solve
+lemma "|- []P \<longrightarrow> []<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> <>P" by S43_solve
+lemma "|- []<>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> <>[]<>P" by S43_solve
+lemma "|- <>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "|- []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
+lemma "|- <>[]<>P \<longleftrightarrow> []<>P" by S43_solve
 
-lemma "|- []P | []Q --> [](P | Q)" by S43_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by S43_solve
-lemma "|- [](P | Q) --> []P | <>Q" by S43_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by S43_solve
-lemma "|- [](P | Q) --> <>P | []Q" by S43_solve
-lemma "|- [](P | Q) --> []<>P | []<>Q" by S43_solve
-lemma "|- <>[]P & <>[]Q --> <>(P & Q)" by S43_solve
-lemma "|- <>[](P & Q) <-> <>[]P & <>[]Q" by S43_solve
-lemma "|- []<>(P | Q) <-> []<>P | []<>Q" by S43_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
+lemma "|- <>[]P \<and> <>[]Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "|- <>[](P \<and> Q) \<longleftrightarrow> <>[]P \<and> <>[]Q" by S43_solve
+lemma "|- []<>(P \<or> Q) \<longleftrightarrow> []<>P \<or> []<>Q" by S43_solve
 
 end
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/Sequents.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -19,9 +19,7 @@
 
 subsection \<open>Sequences\<close>
 
-typedecl
- seq'
-
+typedecl seq'
 consts
  SeqO'         :: "[o,seq']=>seq'"
  Seq1'         :: "o=>seq'"
@@ -149,4 +147,3 @@
 ML_file "prover.ML"
 
 end
-
diff -r 9f5145281888 -r 538100cc4399 src/Sequents/T.thy
--- a/src/Sequents/T.thy	Sat Oct 10 19:22:05 2015 +0200
+++ b/src/Sequents/T.thy	Sat Oct 10 20:51:39 2015 +0200
@@ -13,22 +13,22 @@
 (*                delta * == {P | <>P : delta}                  *)
 
   lstar0:         "|L>" and
-  lstar1:         "$G |L> $H ==> []P, $G |L> P, $H" and
-  lstar2:         "$G |L> $H ==>   P, $G |L>    $H" and
+  lstar1:         "$G |L> $H \<Longrightarrow> []P, $G |L> P, $H" and
+  lstar2:         "$G |L> $H \<Longrightarrow>   P, $G |L>    $H" and
   rstar0:         "|R>" and
-  rstar1:         "$G |R> $H ==> <>P, $G |R> P, $H" and
-  rstar2:         "$G |R> $H ==>   P, $G |R>    $H" and
+  rstar1:         "$G |R> $H \<Longrightarrow> <>P, $G |R> P, $H" and
+  rstar2:         "$G |R> $H \<Longrightarrow>   P, $G |R>    $H" and
 
 (* Rules for [] and <> *)
 
   boxR:
-   "[| $E |L> $E';  $F |R> $F';  $G |R> $G';
-               $E'        |- $F', P, $G'|] ==> $E          |- $F, []P, $G" and
-  boxL:     "$E, P, $F  |-         $G    ==> $E, []P, $F |-          $G" and
-  diaR:     "$E         |- $F, P,  $G    ==> $E          |- $F, <>P, $G" and
+   "\<lbrakk>$E |L> $E';  $F |R> $F';  $G |R> $G';
+               $E'        |- $F', P, $G'\<rbrakk> \<Longrightarrow> $E          |- $F, []P, $G" and
+  boxL:     "$E, P, $F  |-         $G    \<Longrightarrow> $E, []P, $F |-          $G" and
+  diaR:     "$E         |- $F, P,  $G    \<Longrightarrow> $E          |- $F, <>P, $G" and
   diaL:
-   "[| $E |L> $E';  $F |L> $F';  $G |R> $G';
-               $E', P, $F'|-         $G'|] ==> $E, <>P, $F |-          $G"
+   "\<lbrakk>$E |L> $E';  $F |L> $F';  $G |R> $G';
+               $E', P, $F'|-         $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F |-          $G"
 
 ML \<open>
 structure T_Prover = Modal_ProverFun
@@ -47,28 +47,28 @@
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
 
-lemma "|- []P --> P" by T_solve
-lemma "|- [](P-->Q) --> ([]P-->[]Q)" by T_solve   (* normality*)
-lemma "|- (P--<Q) --> []P --> []Q" by T_solve
-lemma "|- P --> <>P" by T_solve
+lemma "|- []P \<longrightarrow> P" by T_solve
+lemma "|- [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by T_solve   (* normality*)
+lemma "|- (P --< Q) \<longrightarrow> []P \<longrightarrow> []Q" by T_solve
+lemma "|- P \<longrightarrow> <>P" by T_solve
 
-lemma "|-  [](P & Q) <-> []P & []Q" by T_solve
-lemma "|-  <>(P | Q) <-> <>P | <>Q" by T_solve
-lemma "|-  [](P<->Q) <-> (P>-<Q)" by T_solve
-lemma "|-  <>(P-->Q) <-> ([]P--><>Q)" by T_solve
-lemma "|-        []P <-> ~<>(~P)" by T_solve
-lemma "|-     [](~P) <-> ~<>P" by T_solve
-lemma "|-       ~[]P <-> <>(~P)" by T_solve
-lemma "|-      [][]P <-> ~<><>(~P)" by T_solve
-lemma "|- ~<>(P | Q) <-> ~<>P & ~<>Q" by T_solve
+lemma "|-  [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by T_solve
+lemma "|-  <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by T_solve
+lemma "|-  [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >-< Q)" by T_solve
+lemma "|-  <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by T_solve
+lemma "|-        []P \<longleftrightarrow> \<not> <>(\<not> P)" by T_solve
+lemma "|-     [](\<not> P) \<longleftrightarrow> \<not> <>P" by T_solve
+lemma "|-       \<not> []P \<longleftrightarrow> <>(\<not> P)" by T_solve
+lemma "|-      [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by T_solve
+lemma "|- \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>Q" by T_solve
 
-lemma "|- []P | []Q --> [](P | Q)" by T_solve
-lemma "|- <>(P & Q) --> <>P & <>Q" by T_solve
-lemma "|- [](P | Q) --> []P | <>Q" by T_solve
-lemma "|- <>P & []Q --> <>(P & Q)" by T_solve
-lemma "|- [](P | Q) --> <>P | []Q" by T_solve
-lemma "|- <>(P-->(Q & R)) --> ([]P --> <>Q) & ([]P--><>R)" by T_solve
-lemma "|- (P--<Q) & (Q--<R) --> (P--<R)" by T_solve
-lemma "|- []P --> <>Q --> <>(P & Q)" by T_solve
+lemma "|- []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by T_solve
+lemma "|- <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by T_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by T_solve
+lemma "|- <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by T_solve
+lemma "|- [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by T_solve
+lemma "|- <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by T_solve
+lemma "|- (P --< Q) \<and> (Q --< R ) \<longrightarrow> (P --< R)" by T_solve
+lemma "|- []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by T_solve
 
 end