# HG changeset patch
# User wenzelm
# Date 1444503284 -7200
# Node ID 0a29a984a91b344aea33547060b051c298c9d239
# Parent  538100cc4399e81ad07b3e70a652a4fffee99122
more symbols;

diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/ILL.thy
--- a/src/Sequents/ILL.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/ILL.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -31,7 +31,7 @@
   PromAux :: "three_seqi"
 
 syntax
-  "_Trueprop" :: "single_seqe" ("((_)/ |- (_))" [6,6] 5)
+  "_Trueprop" :: "single_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
   "_Context"  :: "two_seqe"   ("((_)/ :=: (_))" [6,6] 5)
   "_PromAux"  :: "three_seqe" ("promaux {_||_||_}")
 
@@ -56,63 +56,63 @@
 
 axiomatization where
 
-identity:        "P |- P" and
+identity:        "P \<turnstile> P" and
 
-zerol:           "$G, 0, $H |- A" and
+zerol:           "$G, 0, $H \<turnstile> A" and
 
   (* RULES THAT DO NOT DIVIDE CONTEXT *)
 
-derelict:   "$F, A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and
+derelict:   "$F, A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
   (* unfortunately, this one removes !A  *)
 
-contract:  "$F, !A, !A, $G |- C \<Longrightarrow> $F, !A, $G |- C" and
+contract:  "$F, !A, !A, $G \<turnstile> C \<Longrightarrow> $F, !A, $G \<turnstile> C" and
 
-weaken:     "$F, $G |- C \<Longrightarrow> $G, !A, $F |- C" and
+weaken:     "$F, $G \<turnstile> C \<Longrightarrow> $G, !A, $F \<turnstile> C" and
   (* weak form of weakening, in practice just to clean context *)
   (* weaken and contract not needed (CHECK)  *)
 
-promote2:        "promaux{ || $H || B} \<Longrightarrow> $H |- !B" and
+promote2:        "promaux{ || $H || B} \<Longrightarrow> $H \<turnstile> !B" and
 promote1:        "promaux{!A, $G || $H || B}
                   \<Longrightarrow> promaux {$G || $H, !A || B}" and
-promote0:        "$G |- A \<Longrightarrow> promaux {$G || || A}" and
+promote0:        "$G \<turnstile> A \<Longrightarrow> promaux {$G || || A}" and
 
 
 
-tensl:     "$H, A, B, $G |- C \<Longrightarrow> $H, A >< B, $G |- C" and
+tensl:     "$H, A, B, $G \<turnstile> C \<Longrightarrow> $H, A >< B, $G \<turnstile> C" and
 
-impr:      "A, $F |- B \<Longrightarrow> $F |- A -o B" and
+impr:      "A, $F \<turnstile> B \<Longrightarrow> $F \<turnstile> A -o B" and
 
-conjr:           "\<lbrakk>$F |- A ;
-                 $F |- B\<rbrakk>
-                \<Longrightarrow> $F |- (A && B)" and
+conjr:           "\<lbrakk>$F \<turnstile> A ;
+                 $F \<turnstile> B\<rbrakk>
+                \<Longrightarrow> $F \<turnstile> (A && B)" and
 
-conjll:          "$G, A, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and
+conjll:          "$G, A, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> C" and
 
-conjlr:          "$G, B, $H |- C \<Longrightarrow> $G, A && B, $H |- C" and
+conjlr:          "$G, B, $H \<turnstile> C \<Longrightarrow> $G, A && B, $H \<turnstile> 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
+disjrl:          "$G \<turnstile> A \<Longrightarrow> $G \<turnstile> A ++ B" and
+disjrr:          "$G \<turnstile> B \<Longrightarrow> $G \<turnstile> A ++ B" and
+disjl:           "\<lbrakk>$G, A, $H \<turnstile> C ;
+                   $G, B, $H \<turnstile> C\<rbrakk>
+                 \<Longrightarrow> $G, A ++ B, $H \<turnstile> C" and
 
 
       (* RULES THAT DIVIDE CONTEXT *)
 
 tensr:           "\<lbrakk>$F, $J :=: $G;
-                   $F |- A ;
-                   $J |- B\<rbrakk>
-                     \<Longrightarrow> $G |- A >< B" and
+                   $F \<turnstile> A ;
+                   $J \<turnstile> B\<rbrakk>
+                     \<Longrightarrow> $G \<turnstile> A >< B" and
 
 impl:            "\<lbrakk>$G, $F :=: $J, $H ;
-                   B, $F |- C ;
-                   $G |- A\<rbrakk>
-                     \<Longrightarrow> $J, A -o B, $H |- C" and
+                   B, $F \<turnstile> C ;
+                   $G \<turnstile> A\<rbrakk>
+                     \<Longrightarrow> $J, A -o B, $H \<turnstile> C" 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
+        $H1, $H2, $H3, $H4 \<turnstile> A ;
+        $J1, $J2, A, $J3, $J4 \<turnstile> B\<rbrakk> \<Longrightarrow> $F \<turnstile> B" and
 
 
   (* CONTEXT RULES *)
@@ -150,7 +150,7 @@
   zerol
   identity
 
-lemma aux_impl: "$F, $G |- A \<Longrightarrow> $F, !(A -o B), $G |- B"
+lemma aux_impl: "$F, $G \<turnstile> A \<Longrightarrow> $F, !(A -o B), $G \<turnstile> B"
   apply (rule derelict)
   apply (rule impl)
   apply (rule_tac [2] identity)
@@ -158,16 +158,16 @@
   apply assumption
   done
 
-lemma conj_lemma: " $F, !A, !B, $G |- C \<Longrightarrow> $F, !(A && B), $G |- C"
+lemma conj_lemma: " $F, !A, !B, $G \<turnstile> C \<Longrightarrow> $F, !(A && B), $G \<turnstile> C"
   apply (rule contract)
   apply (rule_tac A = " (!A) >< (!B) " in cut)
   apply (rule_tac [2] tensr)
   prefer 3
-  apply (subgoal_tac "! (A && B) |- !A")
+  apply (subgoal_tac "! (A && B) \<turnstile> !A")
   apply assumption
   apply best
   prefer 3
-  apply (subgoal_tac "! (A && B) |- !B")
+  apply (subgoal_tac "! (A && B) \<turnstile> !B")
   apply assumption
   apply best
   apply (rule_tac [2] context1)
@@ -178,20 +178,20 @@
   apply (rule context1)
   done
 
-lemma impr_contract: "!A, !A, $G |- B \<Longrightarrow> $G |- (!A) -o B"
+lemma impr_contract: "!A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B"
   apply (rule impr)
   apply (rule contract)
   apply assumption
   done
 
-lemma impr_contr_der: "A, !A, $G |- B \<Longrightarrow> $G |- (!A) -o B"
+lemma impr_contr_der: "A, !A, $G \<turnstile> B \<Longrightarrow> $G \<turnstile> (!A) -o B"
   apply (rule impr)
   apply (rule contract)
   apply (rule derelict)
   apply assumption
   done
 
-lemma contrad1: "$F, (!B) -o 0, $G, !B, $H |- A"
+lemma contrad1: "$F, (!B) -o 0, $G, !B, $H \<turnstile> A"
   apply (rule impl)
   apply (rule_tac [3] identity)
   apply (rule context3)
@@ -200,7 +200,7 @@
   done
 
 
-lemma contrad2: "$F, !B, $G, (!B) -o 0, $H |- A"
+lemma contrad2: "$F, !B, $G, (!B) -o 0, $H \<turnstile> A"
   apply (rule impl)
   apply (rule_tac [3] identity)
   apply (rule context3)
@@ -208,14 +208,14 @@
   apply (rule zerol)
   done
 
-lemma ll_mp: "A -o B, A |- B"
+lemma ll_mp: "A -o B, A \<turnstile> B"
   apply (rule impl)
   apply (rule_tac [2] identity)
   apply (rule_tac [2] identity)
   apply (rule context1)
   done
 
-lemma mp_rule1: "$F, B, $G, $H |- C \<Longrightarrow> $F, A, $G, A -o B, $H |- C"
+lemma mp_rule1: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A, $G, A -o B, $H \<turnstile> C"
   apply (rule_tac A = "B" in cut)
   apply (rule_tac [2] ll_mp)
   prefer 2 apply (assumption)
@@ -224,7 +224,7 @@
   apply (rule context1)
   done
 
-lemma mp_rule2: "$F, B, $G, $H |- C \<Longrightarrow> $F, A -o B, $G, A, $H |- C"
+lemma mp_rule2: "$F, B, $G, $H \<turnstile> C \<Longrightarrow> $F, A -o B, $G, A, $H \<turnstile> C"
   apply (rule_tac A = "B" in cut)
   apply (rule_tac [2] ll_mp)
   prefer 2 apply (assumption)
@@ -233,11 +233,11 @@
   apply (rule context1)
   done
 
-lemma or_to_and: "!((!(A ++ B)) -o 0) |- !( ((!A) -o 0) && ((!B) -o 0))"
+lemma or_to_and: "!((!(A ++ B)) -o 0) \<turnstile> !( ((!A) -o 0) && ((!B) -o 0))"
   by best
 
-lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G |- C \<Longrightarrow>
-          $F, !((!(A ++ B)) -o 0), $G |- C"
+lemma o_a_rule: "$F, !( ((!A) -o 0) && ((!B) -o 0)), $G \<turnstile> C \<Longrightarrow>
+          $F, !((!(A ++ B)) -o 0), $G \<turnstile> C"
   apply (rule cut)
   apply (rule_tac [2] or_to_and)
   prefer 2 apply (assumption)
@@ -245,17 +245,17 @@
   apply (rule context1)
   done
 
-lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) |- (!(A && B)) -o C"
+lemma conj_imp: "((!A) -o C) ++ ((!B) -o C) \<turnstile> (!(A && B)) -o C"
   apply (rule impr)
   apply (rule conj_lemma)
   apply (rule disjl)
   apply (rule mp_rule1, best)+
   done
 
-lemma not_imp: "!A, !((!B) -o 0) |- (!((!A) -o B)) -o 0"
+lemma not_imp: "!A, !((!B) -o 0) \<turnstile> (!((!A) -o B)) -o 0"
   by best
 
-lemma a_not_a: "!A -o (!A -o 0) |- !A -o 0"
+lemma a_not_a: "!A -o (!A -o 0) \<turnstile> !A -o 0"
   apply (rule impr)
   apply (rule contract)
   apply (rule impl)
@@ -264,7 +264,7 @@
   apply best
   done
 
-lemma a_not_a_rule: "$J1, !A -o 0, $J2 |- B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 |- B"
+lemma a_not_a_rule: "$J1, !A -o 0, $J2 \<turnstile> B \<Longrightarrow> $J1, !A -o (!A -o 0), $J2 \<turnstile> B"
   apply (rule_tac A = "!A -o 0" in cut)
   apply (rule_tac [2] a_not_a)
   prefer 2 apply assumption
@@ -294,17 +294,17 @@
 
 (* Some examples from Troelstra and van Dalen *)
 
-lemma "!((!A) -o ((!B) -o 0)) |- (!(A && B)) -o 0"
+lemma "!((!A) -o ((!B) -o 0)) \<turnstile> (!(A && B)) -o 0"
   by best_safe
 
-lemma "!((!(A && B)) -o 0) |- !((!A) -o ((!B) -o 0))"
+lemma "!((!(A && B)) -o 0) \<turnstile> !((!A) -o ((!B) -o 0))"
   by best_safe
 
-lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) |-
+lemma "!( (!((! ((!A) -o B) ) -o 0)) -o 0) \<turnstile>
         (!A) -o ( (!  ((!B) -o 0)) -o 0)"
   by best_safe
 
-lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) |-
+lemma "!(  (!A) -o ( (!  ((!B) -o 0)) -o 0) ) \<turnstile>
           (!((! ((!A) -o B) ) -o 0)) -o 0"
   by best_power
 
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/ILL_predlog.thy
--- a/src/Sequents/ILL_predlog.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/ILL_predlog.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -30,100 +30,100 @@
 
 (* from [kleene 52] pp 118,119 *)
 
-lemma k49a: "|- [* A > ( - ( - A)) *]"
+lemma k49a: "\<turnstile> [* A > ( - ( - A)) *]"
   by best_safe
 
-lemma k49b: "|- [*( - ( - ( - A))) = ( - A)*]"
+lemma k49b: "\<turnstile> [*( - ( - ( - A))) = ( - A)*]"
   by best_safe
 
-lemma k49c: "|- [* (A | - A) > ( - - A = A) *]"
+lemma k49c: "\<turnstile> [* (A | - A) > ( - - A = A) *]"
   by best_safe
 
-lemma k50a: "|- [* - (A = - A) *]"
+lemma k50a: "\<turnstile> [* - (A = - A) *]"
   by best_power
 
-lemma k51a: "|- [* - - (A | - A) *]"
+lemma k51a: "\<turnstile> [* - - (A | - A) *]"
   by best_safe
 
-lemma k51b: "|- [* - - (- - A > A) *]"
+lemma k51b: "\<turnstile> [* - - (- - A > A) *]"
   by best_power
 
-lemma k56a: "|- [* (A | B) > - (- A & - B) *]"
+lemma k56a: "\<turnstile> [* (A | B) > - (- A & - B) *]"
   by best_safe
 
-lemma k56b: "|- [* (-A | B) > - (A & -B) *]"
+lemma k56b: "\<turnstile> [* (-A | B) > - (A & -B) *]"
   by best_safe
 
-lemma k57a: "|- [* (A & B) > - (-A | -B) *]"
+lemma k57a: "\<turnstile> [* (A & B) > - (-A | -B) *]"
   by best_safe
 
-lemma k57b: "|- [* (A & -B) > -(-A | B) *]"
+lemma k57b: "\<turnstile> [* (A & -B) > -(-A | B) *]"
   by best_power
 
-lemma k58a: "|- [* (A > B) > - (A & -B) *]"
+lemma k58a: "\<turnstile> [* (A > B) > - (A & -B) *]"
   by best_safe
 
-lemma k58b: "|- [* (A > -B) = -(A & B) *]"
+lemma k58b: "\<turnstile> [* (A > -B) = -(A & B) *]"
   by best_safe
 
-lemma k58c: "|- [* - (A & B) = (- - A > - B) *]"
+lemma k58c: "\<turnstile> [* - (A & B) = (- - A > - B) *]"
   by best_safe
 
-lemma k58d: "|- [* (- - A > - B) = - - (-A | -B) *]"
+lemma k58d: "\<turnstile> [* (- - A > - B) = - - (-A | -B) *]"
   by best_safe
 
-lemma k58e: "! [* - -B > B *] |- [* (- -A > B) = (A > B) *]"
+lemma k58e: "! [* - -B > B *] \<turnstile> [* (- -A > B) = (A > B) *]"
   by best_safe
 
-lemma k58f: "! [* - -B > B *] |- [* (A > B) = - (A & -B) *]"
+lemma k58f: "! [* - -B > B *] \<turnstile> [* (A > B) = - (A & -B) *]"
   by best_safe
 
-lemma k58g: "|- [* (- -A > B) > - (A & -B) *]"
+lemma k58g: "\<turnstile> [* (- -A > B) > - (A & -B) *]"
   by best_safe
 
-lemma k59a: "|- [* (-A | B) > (A > B) *]"
+lemma k59a: "\<turnstile> [* (-A | B) > (A > B) *]"
   by best_safe
 
-lemma k59b: "|- [* (A > B) > - - (-A | B) *]"
+lemma k59b: "\<turnstile> [* (A > B) > - - (-A | B) *]"
   by best_power
 
-lemma k59c: "|- [* (-A > B) > - -(A | B) *]"
+lemma k59c: "\<turnstile> [* (-A > B) > - -(A | B) *]"
   by best_power
 
-lemma k60a: "|- [* (A & B) > - (A > -B) *]"
+lemma k60a: "\<turnstile> [* (A & B) > - (A > -B) *]"
   by best_safe
 
-lemma k60b: "|- [* (A & -B) > - (A > B) *]"
+lemma k60b: "\<turnstile> [* (A & -B) > - (A > B) *]"
   by best_safe
 
-lemma k60c: "|- [* ( - - A & B) > - (A > -B) *]"
+lemma k60c: "\<turnstile> [* ( - - A & B) > - (A > -B) *]"
   by best_safe
 
-lemma k60d: "|- [* (- - A & - B) = - (A > B) *]"
+lemma k60d: "\<turnstile> [* (- - A & - B) = - (A > B) *]"
   by best_safe
 
-lemma k60e: "|- [* - (A > B) = - (-A | B) *]"
+lemma k60e: "\<turnstile> [* - (A > B) = - (-A | B) *]"
   by best_safe
 
-lemma k60f: "|- [* - (-A | B) = - - (A & -B) *]"
+lemma k60f: "\<turnstile> [* - (-A | B) = - - (A & -B) *]"
   by best_safe
 
-lemma k60g: "|- [* - - (A > B) = - (A & -B) *]"
+lemma k60g: "\<turnstile> [* - - (A > B) = - (A & -B) *]"
   by best_power
 
-lemma k60h: "|- [* - (A & -B) = (A > - -B) *]"
+lemma k60h: "\<turnstile> [* - (A & -B) = (A > - -B) *]"
   by best_safe
 
-lemma k60i: "|- [* (A > - -B) = (- -A > - -B) *]"
+lemma k60i: "\<turnstile> [* (A > - -B) = (- -A > - -B) *]"
   by best_safe
 
-lemma k61a: "|- [* (A | B) > (-A > B) *]"
+lemma k61a: "\<turnstile> [* (A | B) > (-A > B) *]"
   by best_safe
 
-lemma k61b: "|- [* - (A | B) = - (-A > B) *]"
+lemma k61b: "\<turnstile> [* - (A | B) = - (-A > B) *]"
   by best_power
 
-lemma k62a: "|- [* (-A | -B) > - (A & B) *]"
+lemma k62a: "\<turnstile> [* (-A | -B) > - (A & B) *]"
   by best_safe
 
 end
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/LK.thy
--- a/src/Sequents/LK.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/LK.thy	Sat Oct 10 20:54:44 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 \<Longrightarrow>, needed for instance to prove imp_cong.
+link between \<turnstile> 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,65 +17,65 @@
 begin
 
 axiomatization where
-  monotonic:  "($H |- P \<Longrightarrow> $H |- Q) \<Longrightarrow> $H, P |- Q" and
+  monotonic:  "($H \<turnstile> P \<Longrightarrow> $H \<turnstile> Q) \<Longrightarrow> $H, P \<turnstile> Q" and
 
-  left_cong:  "\<lbrakk>P == P';  |- P' \<Longrightarrow> ($H |- $F) \<equiv> ($H' |- $F')\<rbrakk>
-               \<Longrightarrow> (P, $H |- $F) \<equiv> (P', $H' |- $F')"
+  left_cong:  "\<lbrakk>P == P';  \<turnstile> P' \<Longrightarrow> ($H \<turnstile> $F) \<equiv> ($H' \<turnstile> $F')\<rbrakk>
+               \<Longrightarrow> (P, $H \<turnstile> $F) \<equiv> (P', $H' \<turnstile> $F')"
 
 
 subsection \<open>Rewrite rules\<close>
 
 lemma conj_simps:
-  "|- 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)"
+  "\<turnstile> P \<and> True \<longleftrightarrow> P"
+  "\<turnstile> True \<and> P \<longleftrightarrow> P"
+  "\<turnstile> P \<and> False \<longleftrightarrow> False"
+  "\<turnstile> False \<and> P \<longleftrightarrow> False"
+  "\<turnstile> P \<and> P \<longleftrightarrow> P"
+  "\<turnstile> P \<and> P \<and> Q \<longleftrightarrow> P \<and> Q"
+  "\<turnstile> P \<and> \<not> P \<longleftrightarrow> False"
+  "\<turnstile> \<not> P \<and> P \<longleftrightarrow> False"
+  "\<turnstile> (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
   by (fast add!: subst)+
 
 lemma disj_simps:
-  "|- 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)"
+  "\<turnstile> P \<or> True \<longleftrightarrow> True"
+  "\<turnstile> True \<or> P \<longleftrightarrow> True"
+  "\<turnstile> P \<or> False \<longleftrightarrow> P"
+  "\<turnstile> False \<or> P \<longleftrightarrow> P"
+  "\<turnstile> P \<or> P \<longleftrightarrow> P"
+  "\<turnstile> P \<or> P \<or> Q \<longleftrightarrow> P \<or> Q"
+  "\<turnstile> (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
   by (fast add!: subst)+
 
 lemma not_simps:
-  "|- \<not> False \<longleftrightarrow> True"
-  "|- \<not> True \<longleftrightarrow> False"
+  "\<turnstile> \<not> False \<longleftrightarrow> True"
+  "\<turnstile> \<not> True \<longleftrightarrow> False"
   by (fast add!: subst)+
 
 lemma imp_simps:
-  "|- (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"
+  "\<turnstile> (P \<longrightarrow> False) \<longleftrightarrow> \<not> P"
+  "\<turnstile> (P \<longrightarrow> True) \<longleftrightarrow> True"
+  "\<turnstile> (False \<longrightarrow> P) \<longleftrightarrow> True"
+  "\<turnstile> (True \<longrightarrow> P) \<longleftrightarrow> P"
+  "\<turnstile> (P \<longrightarrow> P) \<longleftrightarrow> True"
+  "\<turnstile> (P \<longrightarrow> \<not> P) \<longleftrightarrow> \<not> P"
   by (fast add!: subst)+
 
 lemma iff_simps:
-  "|- (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"
+  "\<turnstile> (True \<longleftrightarrow> P) \<longleftrightarrow> P"
+  "\<turnstile> (P \<longleftrightarrow> True) \<longleftrightarrow> P"
+  "\<turnstile> (P \<longleftrightarrow> P) \<longleftrightarrow> True"
+  "\<turnstile> (False \<longleftrightarrow> P) \<longleftrightarrow> \<not> P"
+  "\<turnstile> (P \<longleftrightarrow> False) \<longleftrightarrow> \<not> P"
   by (fast add!: subst)+
 
 lemma quant_simps:
-  "\<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)"
+  "\<And>P. \<turnstile> (\<forall>x. P) \<longleftrightarrow> P"
+  "\<And>P. \<turnstile> (\<forall>x. x = t \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+  "\<And>P. \<turnstile> (\<forall>x. t = x \<longrightarrow> P(x)) \<longleftrightarrow> P(t)"
+  "\<And>P. \<turnstile> (\<exists>x. P) \<longleftrightarrow> P"
+  "\<And>P. \<turnstile> (\<exists>x. x = t \<and> P(x)) \<longleftrightarrow> P(t)"
+  "\<And>P. \<turnstile> (\<exists>x. t = x \<and> P(x)) \<longleftrightarrow> P(t)"
   by (fast add!: subst)+
 
 
@@ -89,39 +89,39 @@
 
 text \<open>existential miniscoping\<close>
 lemma ex_simps:
-  "\<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))"
+  "\<And>P Q. \<turnstile> (\<exists>x. P(x) \<and> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<and> Q"
+  "\<And>P Q. \<turnstile> (\<exists>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<exists>x. Q(x))"
+  "\<And>P Q. \<turnstile> (\<exists>x. P(x) \<or> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<or> Q"
+  "\<And>P Q. \<turnstile> (\<exists>x. P \<or> Q(x)) \<longleftrightarrow> P \<or> (\<exists>x. Q(x))"
+  "\<And>P Q. \<turnstile> (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+  "\<And>P Q. \<turnstile> (\<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:
-  "\<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))"
+  "\<And>P Q. \<turnstile> (\<forall>x. P(x) \<and> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<and> Q"
+  "\<And>P Q. \<turnstile> (\<forall>x. P \<and> Q(x)) \<longleftrightarrow> P \<and> (\<forall>x. Q(x))"
+  "\<And>P Q. \<turnstile> (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<exists>x. P(x)) \<longrightarrow> Q"
+  "\<And>P Q. \<turnstile> (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> P \<longrightarrow> (\<forall>x. Q(x))"
+  "\<And>P Q. \<turnstile> (\<forall>x. P(x) \<or> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<or> Q"
+  "\<And>P Q. \<turnstile> (\<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 \<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)"
+  "\<turnstile> P \<and> (Q \<or> R) \<longleftrightarrow> P \<and> Q \<or> P \<and> R"
+  "\<turnstile> (Q \<or> R) \<and> P \<longleftrightarrow> Q \<and> P \<or> R \<and> P"
+  "\<turnstile> (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
   by (fast add!: subst)+
 
-lemma P_iff_F: "|- \<not> P \<Longrightarrow> |- (P \<longleftrightarrow> False)"
+lemma P_iff_F: "\<turnstile> \<not> P \<Longrightarrow> \<turnstile> (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 \<Longrightarrow> |- (P \<longleftrightarrow> True)"
+lemma P_iff_T: "\<turnstile> P \<Longrightarrow> \<turnstile> (P \<longleftrightarrow> True)"
   apply (erule thinR [THEN cut])
   apply fast
   done
@@ -130,51 +130,51 @@
 
 
 lemma LK_extra_simps:
-  "|- 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)"
+  "\<turnstile> P \<or> \<not> P"
+  "\<turnstile> \<not> P \<or> P"
+  "\<turnstile> \<not> \<not> P \<longleftrightarrow> P"
+  "\<turnstile> (\<not> P \<longrightarrow> P) \<longleftrightarrow> P"
+  "\<turnstile> (\<not> P \<longleftrightarrow> \<not> Q) \<longleftrightarrow> (P \<longleftrightarrow> Q)"
   by (fast add!: subst)+
 
 
 subsection \<open>Named rewrite rules\<close>
 
-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)"
+lemma conj_commute: "\<turnstile> P \<and> Q \<longleftrightarrow> Q \<and> P"
+  and conj_left_commute: "\<turnstile> 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 \<or> Q \<longleftrightarrow> Q \<or> P"
-  and disj_left_commute: "|- P \<or> (Q \<or> R) \<longleftrightarrow> Q \<or> (P \<or> R)"
+lemma disj_commute: "\<turnstile> P \<or> Q \<longleftrightarrow> Q \<or> P"
+  and disj_left_commute: "\<turnstile> 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 \<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)"
+lemma conj_disj_distribL: "\<turnstile> P \<and> (Q \<or> R) \<longleftrightarrow> (P \<and> Q \<or> P \<and> R)"
+  and conj_disj_distribR: "\<turnstile> (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R \<or> Q \<and> 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 disj_conj_distribL: "\<turnstile> P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+  and disj_conj_distribR: "\<turnstile> (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> 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_conj_distrib: "\<turnstile> (P \<longrightarrow> (Q \<and> R)) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
+  and imp_conj: "\<turnstile> ((P \<and> Q) \<longrightarrow> R)  \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
+  and imp_disj: "\<turnstile> (P \<or> Q \<longrightarrow> R)  \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> 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 imp_disj1: "\<turnstile> (P \<longrightarrow> Q) \<or> R \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
+  and imp_disj2: "\<turnstile> Q \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
 
-  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 de_Morgan_disj: "\<turnstile> (\<not> (P \<or> Q)) \<longleftrightarrow> (\<not> P \<and> \<not> Q)"
+  and de_Morgan_conj: "\<turnstile> (\<not> (P \<and> Q)) \<longleftrightarrow> (\<not> P \<or> \<not> Q)"
 
-  and not_iff: "|- \<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)"
+  and not_iff: "\<turnstile> \<not> (P \<longleftrightarrow> Q) \<longleftrightarrow> (P \<longleftrightarrow> \<not> Q)"
   by (fast add!: subst)+
 
 lemma imp_cong:
-  assumes p1: "|- P \<longleftrightarrow> P'"
-    and p2: "|- P' \<Longrightarrow> |- Q \<longleftrightarrow> Q'"
-  shows "|- (P \<longrightarrow> Q) \<longleftrightarrow> (P' \<longrightarrow> Q')"
+  assumes p1: "\<turnstile> P \<longleftrightarrow> P'"
+    and p2: "\<turnstile> P' \<Longrightarrow> \<turnstile> Q \<longleftrightarrow> Q'"
+  shows "\<turnstile> (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 \<longleftrightarrow> P'"
-    and p2: "|- P' \<Longrightarrow> |- Q \<longleftrightarrow> Q'"
-  shows "|- (P \<and> Q) \<longleftrightarrow> (P' \<and> Q')"
+  assumes p1: "\<turnstile> P \<longleftrightarrow> P'"
+    and p2: "\<turnstile> P' \<Longrightarrow> \<turnstile> Q \<longleftrightarrow> Q'"
+  shows "\<turnstile> (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 \<longleftrightarrow> y = x"
+lemma eq_sym_conv: "\<turnstile> x = y \<longleftrightarrow> y = x"
   by (fast add!: subst)
 
 ML_file "simpdata.ML"
@@ -207,10 +207,10 @@
 
 text \<open>To create substition rules\<close>
 
-lemma eq_imp_subst: "|- a = b \<Longrightarrow> $H, A(a), $G |- $E, A(b), $F"
+lemma eq_imp_subst: "\<turnstile> a = b \<Longrightarrow> $H, A(a), $G \<turnstile> $E, A(b), $F"
   by simp
 
-lemma split_if: "|- P(if Q then x else y) \<longleftrightarrow> ((Q \<longrightarrow> P(x)) \<and> (\<not> Q \<longrightarrow> P(y)))"
+lemma split_if: "\<turnstile> 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)
@@ -220,12 +220,12 @@
   apply fast
   done
 
-lemma if_cancel: "|- (if P then x else x) = x"
+lemma if_cancel: "\<turnstile> (if P then x else x) = x"
   apply (lem split_if)
   apply fast
   done
 
-lemma if_eq_cancel: "|- (if x = y then y else x) = x"
+lemma if_eq_cancel: "\<turnstile> (if x = y then y else x) = x"
   apply (lem split_if)
   apply safe
   apply (rule symL)
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/LK/Hard_Quantifiers.thy
--- a/src/Sequents/LK/Hard_Quantifiers.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/LK/Hard_Quantifiers.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -15,68 +15,68 @@
 imports "../LK"
 begin
 
-lemma "|- (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
+lemma "\<turnstile> (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
   by fast
 
-lemma "|- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
+lemma "\<turnstile> (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
   by fast
 
-lemma "|- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+lemma "\<turnstile> (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
   by fast
 
-lemma "|- (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
+lemma "\<turnstile> (\<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 \<forall>*)
-lemma "|- (\<forall>x. P(x) \<longrightarrow> P(f(x))) \<and> P(d) \<longrightarrow> P(f(f(f(d))))"
+lemma "\<turnstile> (\<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 "|- \<exists>x. P(x) \<longrightarrow> P(a) \<and> P(b)"
+lemma "\<turnstile> \<exists>x. P(x) \<longrightarrow> P(a) \<and> P(b)"
   by fast_dup
 
-lemma "|- \<exists>z. P(z) \<longrightarrow> (\<forall>x. P(x))"
+lemma "\<turnstile> \<exists>z. P(z) \<longrightarrow> (\<forall>x. P(x))"
   by best_dup
 
 
 text "Hard examples with quantifiers"
 
 text "Problem 18"
-lemma "|- \<exists>y. \<forall>x. P(y)\<longrightarrow>P(x)"
+lemma "\<turnstile> \<exists>y. \<forall>x. P(y)\<longrightarrow>P(x)"
   by best_dup
 
 text "Problem 19"
-lemma "|- \<exists>x. \<forall>y z. (P(y)\<longrightarrow>Q(z)) \<longrightarrow> (P(x)\<longrightarrow>Q(x))"
+lemma "\<turnstile> \<exists>x. \<forall>y z. (P(y)\<longrightarrow>Q(z)) \<longrightarrow> (P(x)\<longrightarrow>Q(x))"
   by best_dup
 
 text "Problem 20"
-lemma "|- (\<forall>x y. \<exists>z. \<forall>w. (P(x) \<and> Q(y)\<longrightarrow>R(z) \<and> S(w)))
+lemma "\<turnstile> (\<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 "|- (\<exists>x. P \<longrightarrow> Q(x)) \<and> (\<exists>x. Q(x) \<longrightarrow> P) \<longrightarrow> (\<exists>x. P \<longleftrightarrow> Q(x))"
+lemma "\<turnstile> (\<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 "|- (\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
+lemma "\<turnstile> (\<forall>x. P \<longleftrightarrow> Q(x)) \<longrightarrow> (P \<longleftrightarrow> (\<forall>x. Q(x)))"
   by fast
 
 text "Problem 23"
-lemma "|- (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x)))"
+lemma "\<turnstile> (\<forall>x. P \<or> Q(x)) \<longleftrightarrow> (P \<or> (\<forall>x. Q(x)))"
   by best
 
 text "Problem 24"
-lemma "|- \<not> (\<exists>x. S(x) \<and> Q(x)) \<and> (\<forall>x. P(x) \<longrightarrow> Q(x) \<or> R(x)) \<and>
+lemma "\<turnstile> \<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 "|- (\<exists>x. P(x)) \<and>
+lemma "\<turnstile> (\<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)))
@@ -84,13 +84,13 @@
   by best
 
 text "Problem 26"
-lemma "|- ((\<exists>x. p(x)) \<longleftrightarrow> (\<exists>x. q(x))) \<and>
+lemma "\<turnstile> ((\<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 "|- (\<exists>x. P(x) \<and> \<not> Q(x)) \<and>
+lemma "\<turnstile> (\<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)))
@@ -98,57 +98,57 @@
   by pc
 
 text "Problem 28.  AMENDED"
-lemma "|- (\<forall>x. P(x) \<longrightarrow> (\<forall>x. Q(x))) \<and>
+lemma "\<turnstile> (\<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 "|- (\<exists>x. P(x)) \<and> (\<exists>y. Q(y))
+lemma "\<turnstile> (\<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 "|- (\<forall>x. P(x) \<or> Q(x) \<longrightarrow> \<not> R(x)) \<and>
+lemma "\<turnstile> (\<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 "|- \<not> (\<exists>x. P(x) \<and> (Q(x) \<or> R(x))) \<and>
+lemma "\<turnstile> \<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 "|- (\<forall>x. P(x) \<and> (Q(x) \<or> R(x)) \<longrightarrow> S(x)) \<and>
+lemma "\<turnstile> (\<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 "|- (\<forall>x. P(a) \<and> (P(x) \<longrightarrow> P(b)) \<longrightarrow> P(c)) \<longleftrightarrow>
+lemma "\<turnstile> (\<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 "|- ((\<exists>x. \<forall>y. p(x) \<longleftrightarrow> p(y))  \<longleftrightarrow>
+lemma "\<turnstile> ((\<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 "|- \<exists>x y. P(x,y) \<longrightarrow> (\<forall>u v. P(u,v))"
+lemma "\<turnstile> \<exists>x y. P(x,y) \<longrightarrow> (\<forall>u v. P(u,v))"
   by best_dup
 
 text "Problem 36"
-lemma "|- (\<forall>x. \<exists>y. J(x,y)) \<and>
+lemma "\<turnstile> (\<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)))
@@ -156,7 +156,7 @@
   by fast
 
 text "Problem 37"
-lemma "|- (\<forall>z. \<exists>w. \<forall>x. \<exists>y.
+lemma "\<turnstile> (\<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)))
@@ -164,7 +164,7 @@
   by pc
 
 text "Problem 38"
-lemma "|- (\<forall>x. p(a) \<and> (p(x) \<longrightarrow> (\<exists>y. p(y) \<and> r(x,y))) \<longrightarrow>
+lemma "\<turnstile> (\<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>
@@ -172,37 +172,37 @@
   by pc
 
 text "Problem 39"
-lemma "|- \<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
+lemma "\<turnstile> \<not> (\<exists>x. \<forall>y. F(y,x) \<longleftrightarrow> \<not> F(y,y))"
   by fast
 
 text "Problem 40.  AMENDED"
-lemma "|- (\<exists>y. \<forall>x. F(x,y) \<longleftrightarrow> F(x,x)) \<longrightarrow>
+lemma "\<turnstile> (\<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 "|- (\<forall>z. \<exists>y. \<forall>x. f(x,y) \<longleftrightarrow> f(x,z) \<and> \<not> f(x,x))
+lemma "\<turnstile> (\<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 "|- \<not> (\<exists>y. \<forall>x. p(x,y) \<longleftrightarrow> \<not> (\<exists>z. p(x,z) \<and> p(z,x)))"
+lemma "\<turnstile> \<not> (\<exists>y. \<forall>x. p(x,y) \<longleftrightarrow> \<not> (\<exists>z. p(x,z) \<and> p(z,x)))"
   oops
 
 text "Problem 43"
-lemma "|- (\<forall>x. \<forall>y. q(x,y) \<longleftrightarrow> (\<forall>z. p(z,x) \<longleftrightarrow> p(z,y)))
+lemma "\<turnstile> (\<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 "|- (\<forall>x. f(x) \<longrightarrow>
+lemma "\<turnstile> (\<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 "|- (\<forall>x. f(x) \<and> (\<forall>y. g(y) \<and> h(x,y) \<longrightarrow> j(x,y))
+lemma "\<turnstile> (\<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))
@@ -214,50 +214,50 @@
 text "Problems (mainly) involving equality or functions"
 
 text "Problem 48"
-lemma "|- (a = b \<or> c = d) \<and> (a = c \<or> b = d) \<longrightarrow> a = d \<or> b = c"
+lemma "\<turnstile> (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 "|- (\<forall>x. P(a,x) \<or> (\<forall>y. P(x,y))) \<longrightarrow> (\<exists>x. \<forall>y. P(x,y))"
+lemma "\<turnstile> (\<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 "|- (\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+lemma "\<turnstile> (\<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 "|- (\<exists>z w. \<forall>x y. P(x,y) \<longleftrightarrow> (x = z \<and> y = w)) \<longrightarrow>
+lemma "\<turnstile> (\<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 "|- (\<forall>x.(\<exists>y. P(y) \<and> x = f(y)) \<longrightarrow> P(x)) \<longleftrightarrow> (\<forall>x. P(x) \<longrightarrow> P(f(x)))"
+lemma "\<turnstile> (\<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)) \<and> P(f(b,c), f(a,c)) \<and>
+lemma "\<turnstile> 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 "|- (\<forall>x y. f(x) = g(y)) \<longrightarrow> (\<forall>x y. f(f(x)) = f(g(y)))"
+lemma "\<turnstile> (\<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 "|- (\<forall>x. P(x) \<longleftrightarrow> \<not> P(f(x))) \<longrightarrow> (\<exists>x. P(x) \<and> \<not> P(f(x)))"
+lemma "\<turnstile> (\<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 "|- \<forall>x. P(x,f(x)) \<longleftrightarrow> (\<exists>y. (\<forall>z. P(z,y) \<longrightarrow> P(z,f(x))) \<and> P(x,y))"
+lemma "\<turnstile> \<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 "|- (\<forall>x. p(a) \<and> (p(x) \<longrightarrow> p(f(x))) \<longrightarrow> p(f(f(x)))) \<longleftrightarrow>
+lemma "\<turnstile> (\<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
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/LK/Nat.thy
--- a/src/Sequents/LK/Nat.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/LK/Nat.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -17,13 +17,13 @@
   Suc :: "nat \<Rightarrow> nat" and
   rec :: "[nat, 'a, [nat,'a] \<Rightarrow> 'a] \<Rightarrow> 'a"
 where
-  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
+  induct:  "\<lbrakk>$H \<turnstile> $E, P(0), $F;
+             \<And>x. $H, P(x) \<turnstile> $E, P(Suc(x)), $F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P(n), $F" 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))"
+  Suc_inject:  "\<turnstile> Suc(m) = Suc(n) \<longrightarrow> m = n" and
+  Suc_neq_0:   "\<turnstile> Suc(m) \<noteq> 0" and
+  rec_0:       "\<turnstile> rec(0,a,f) = a" and
+  rec_Suc:     "\<turnstile> rec(Suc(m), a, f) = f(m, rec(m,a,f))"
 
 definition add :: "[nat, nat] \<Rightarrow> nat"  (infixl "+" 60)
   where "m + n == rec(m, n, \<lambda>x y. Suc(y))"
@@ -31,43 +31,43 @@
 
 declare Suc_neq_0 [simp]
 
-lemma Suc_inject_rule: "$H, $G, m = n |- $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G |- $E"
+lemma Suc_inject_rule: "$H, $G, m = n \<turnstile> $E \<Longrightarrow> $H, Suc(m) = Suc(n), $G \<turnstile> $E"
   by (rule L_of_imp [OF Suc_inject])
 
-lemma Suc_n_not_n: "|- Suc(k) \<noteq> k"
+lemma Suc_n_not_n: "\<turnstile> 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: "\<turnstile> 0 + n = n"
   apply (unfold add_def)
   apply (rule rec_0)
   done
 
-lemma add_Suc: "|- Suc(m) + n = Suc(m + n)"
+lemma add_Suc: "\<turnstile> 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: "\<turnstile> (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: "\<turnstile> 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: "\<turnstile> m + Suc(n) = Suc(m + n)"
   apply (rule_tac n = "m" in induct)
   apply simp_all
   done
 
-lemma "(\<And>n. |- f(Suc(n)) = Suc(f(n))) \<Longrightarrow> |- f(i + j) = i + f(j)"
+lemma "(\<And>n. \<turnstile> f(Suc(n)) = Suc(f(n))) \<Longrightarrow> \<turnstile> f(i + j) = i + f(j)"
   apply (rule_tac n = "i" in induct)
   apply simp_all
   done
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/LK/Propositional.thy
--- a/src/Sequents/LK/Propositional.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/LK/Propositional.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -11,73 +11,73 @@
 
 text "absorptive laws of \<and> and \<or>"
 
-lemma "|- P \<and> P \<longleftrightarrow> P"
+lemma "\<turnstile> P \<and> P \<longleftrightarrow> P"
   by fast_prop
 
-lemma "|- P \<or> P \<longleftrightarrow> P"
+lemma "\<turnstile> P \<or> P \<longleftrightarrow> P"
   by fast_prop
 
 
 text "commutative laws of \<and> and \<or>"
 
-lemma "|- P \<and> Q \<longleftrightarrow> Q \<and> P"
+lemma "\<turnstile> P \<and> Q \<longleftrightarrow> Q \<and> P"
   by fast_prop
 
-lemma "|- P \<or> Q \<longleftrightarrow> Q \<or> P"
+lemma "\<turnstile> P \<or> Q \<longleftrightarrow> Q \<or> P"
   by fast_prop
 
 
 text "associative laws of \<and> and \<or>"
 
-lemma "|- (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
+lemma "\<turnstile> (P \<and> Q) \<and> R \<longleftrightarrow> P \<and> (Q \<and> R)"
   by fast_prop
 
-lemma "|- (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
+lemma "\<turnstile> (P \<or> Q) \<or> R \<longleftrightarrow> P \<or> (Q \<or> R)"
   by fast_prop
 
 
 text "distributive laws of \<and> and \<or>"
 
-lemma "|- (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
+lemma "\<turnstile> (P \<and> Q) \<or> R \<longleftrightarrow> (P \<or> R) \<and> (Q \<or> R)"
   by fast_prop
 
-lemma "|- (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R) \<or> (Q \<and> R)"
+lemma "\<turnstile> (P \<or> Q) \<and> R \<longleftrightarrow> (P \<and> R) \<or> (Q \<and> R)"
   by fast_prop
 
 
 text "Laws involving implication"
 
-lemma "|- (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
+lemma "\<turnstile> (P \<or> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> R) \<and> (Q \<longrightarrow> R)"
   by fast_prop
 
-lemma "|- (P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
+lemma "\<turnstile> (P \<and> Q \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> (Q \<longrightarrow> R))"
   by fast_prop
 
-lemma "|- (P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
+lemma "\<turnstile> (P \<longrightarrow> Q \<and> R) \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (P \<longrightarrow> R)"
   by fast_prop
 
 
 text "Classical theorems"
 
-lemma "|- P \<or> Q \<longrightarrow> P \<or> \<not> P \<and> Q"
+lemma "\<turnstile> P \<or> Q \<longrightarrow> P \<or> \<not> P \<and> Q"
   by fast_prop
 
-lemma "|- (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<or> R)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R) \<longrightarrow> (P \<and> Q \<or> R)"
   by fast_prop
 
-lemma "|- P \<and> Q \<or> \<not> P \<and> R \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
+lemma "\<turnstile> P \<and> Q \<or> \<not> P \<and> R \<longleftrightarrow> (P \<longrightarrow> Q) \<and> (\<not> P \<longrightarrow> R)"
   by fast_prop
 
-lemma "|- (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<or> (P \<longrightarrow> R) \<longleftrightarrow> (P \<longrightarrow> Q \<or> R)"
   by fast_prop
 
 
 (*If and only if*)
 
-lemma "|- (P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
+lemma "\<turnstile> (P \<longleftrightarrow> Q) \<longleftrightarrow> (Q \<longleftrightarrow> P)"
   by fast_prop
 
-lemma "|- \<not> (P \<longleftrightarrow> \<not> P)"
+lemma "\<turnstile> \<not> (P \<longleftrightarrow> \<not> P)"
   by fast_prop
 
 
@@ -89,71 +89,71 @@
 *)
 
 (*1*)
-lemma "|- (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> \<not> P)"
   by fast_prop
 
 (*2*)
-lemma "|- \<not> \<not> P \<longleftrightarrow> P"
+lemma "\<turnstile> \<not> \<not> P \<longleftrightarrow> P"
   by fast_prop
 
 (*3*)
-lemma "|- \<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
+lemma "\<turnstile> \<not> (P \<longrightarrow> Q) \<longrightarrow> (Q \<longrightarrow> P)"
   by fast_prop
 
 (*4*)
-lemma "|- (\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
+lemma "\<turnstile> (\<not> P \<longrightarrow> Q) \<longleftrightarrow> (\<not> Q \<longrightarrow> P)"
   by fast_prop
 
 (*5*)
-lemma "|- ((P \<or> Q) \<longrightarrow> (P \<or> R)) \<longrightarrow> (P \<or> (Q \<longrightarrow> R))"
+lemma "\<turnstile> ((P \<or> Q) \<longrightarrow> (P \<or> R)) \<longrightarrow> (P \<or> (Q \<longrightarrow> R))"
   by fast_prop
 
 (*6*)
-lemma "|- P \<or> \<not> P"
+lemma "\<turnstile> P \<or> \<not> P"
   by fast_prop
 
 (*7*)
-lemma "|- P \<or> \<not> \<not> \<not> P"
+lemma "\<turnstile> P \<or> \<not> \<not> \<not> P"
   by fast_prop
 
 (*8.  Peirce's law*)
-lemma "|- ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
+lemma "\<turnstile> ((P \<longrightarrow> Q) \<longrightarrow> P) \<longrightarrow> P"
   by fast_prop
 
 (*9*)
-lemma "|- ((P \<or> Q) \<and> (\<not> P \<or> Q) \<and> (P \<or> \<not> Q)) \<longrightarrow> \<not> (\<not> P \<or> \<not> Q)"
+lemma "\<turnstile> ((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 \<longrightarrow> R, R \<longrightarrow> P \<and> Q, P \<longrightarrow> (Q \<or> R) |- P \<longleftrightarrow> Q"
+lemma "Q \<longrightarrow> R, R \<longrightarrow> P \<and> Q, P \<longrightarrow> (Q \<or> R) \<turnstile> P \<longleftrightarrow> Q"
   by fast_prop
 
 (*11.  Proved in each direction (incorrectly, says Pelletier!!)  *)
-lemma "|- P \<longleftrightarrow> P"
+lemma "\<turnstile> P \<longleftrightarrow> P"
   by fast_prop
 
 (*12.  "Dijkstra's law"*)
-lemma "|- ((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
+lemma "\<turnstile> ((P \<longleftrightarrow> Q) \<longleftrightarrow> R) \<longleftrightarrow> (P \<longleftrightarrow> (Q \<longleftrightarrow> R))"
   by fast_prop
 
 (*13.  Distributive law*)
-lemma "|- P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
+lemma "\<turnstile> P \<or> (Q \<and> R) \<longleftrightarrow> (P \<or> Q) \<and> (P \<or> R)"
   by fast_prop
 
 (*14*)
-lemma "|- (P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P))"
+lemma "\<turnstile> (P \<longleftrightarrow> Q) \<longleftrightarrow> ((Q \<or> \<not> P) \<and> (\<not> Q \<or> P))"
   by fast_prop
 
 (*15*)
-lemma "|- (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<longleftrightarrow> (\<not> P \<or> Q)"
   by fast_prop
 
 (*16*)
-lemma "|- (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"
+lemma "\<turnstile> (P \<longrightarrow> Q) \<or> (Q \<longrightarrow> P)"
   by fast_prop
 
 (*17*)
-lemma "|- ((P \<and> (Q \<longrightarrow> R)) \<longrightarrow> S) \<longleftrightarrow> ((\<not> P \<or> Q \<or> S) \<and> (\<not> P \<or> \<not> R \<or> S))"
+lemma "\<turnstile> ((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 538100cc4399 -r 0a29a984a91b src/Sequents/LK/Quantifiers.thy
--- a/src/Sequents/LK/Quantifiers.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/LK/Quantifiers.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -9,94 +9,94 @@
 imports "../LK"
 begin
 
-lemma "|- (\<forall>x. P) \<longleftrightarrow> P"
+lemma "\<turnstile> (\<forall>x. P) \<longleftrightarrow> P"
   by fast
 
-lemma "|- (\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
+lemma "\<turnstile> (\<forall>x y. P(x,y)) \<longleftrightarrow> (\<forall>y x. P(x,y))"
   by fast
 
-lemma "\<forall>u. P(u), \<forall>v. Q(v) |- \<forall>u v. P(u) \<and> Q(v)"
+lemma "\<forall>u. P(u), \<forall>v. Q(v) \<turnstile> \<forall>u v. P(u) \<and> Q(v)"
   by fast
 
 
 text "Permutation of existential quantifier."
 
-lemma "|- (\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
+lemma "\<turnstile> (\<exists>x y. P(x,y)) \<longleftrightarrow> (\<exists>y x. P(x,y))"
   by fast
 
-lemma "|- (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
+lemma "\<turnstile> (\<forall>x. P(x) \<and> Q(x)) \<longleftrightarrow> (\<forall>x. P(x)) \<and> (\<forall>x. Q(x))"
   by fast
 
 (*Converse is invalid*)
-lemma "|- (\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
+lemma "\<turnstile> (\<forall>x. P(x)) \<or> (\<forall>x. Q(x)) \<longrightarrow> (\<forall>x. P(x) \<or> Q(x))"
   by fast
 
 
 text "Pushing \<forall>into an implication."
 
-lemma "|- (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
+lemma "\<turnstile> (\<forall>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<forall>x. Q(x)))"
   by fast
 
-lemma "|- (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
+lemma "\<turnstile> (\<forall>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> Q)"
   by fast
 
-lemma "|- (\<exists>x. P)  \<longleftrightarrow>  P"
+lemma "\<turnstile> (\<exists>x. P)  \<longleftrightarrow>  P"
   by fast
 
 
 text "Distribution of \<exists>over disjunction."
 
-lemma "|- (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
+lemma "\<turnstile> (\<exists>x. P(x) \<or> Q(x)) \<longleftrightarrow> (\<exists>x. P(x)) \<or> (\<exists>x. Q(x))"
   by fast
 
 (*Converse is invalid*)
-lemma "|- (\<exists>x. P(x) \<and> Q(x)) \<longrightarrow> (\<exists>x. P(x)) \<and> (\<exists>x. Q(x))"
+lemma "\<turnstile> (\<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 "|- (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
+lemma "\<turnstile> (\<exists>x. P \<longrightarrow> Q(x)) \<longleftrightarrow> (P \<longrightarrow> (\<exists>x. Q(x)))"
   by fast
 
-lemma "|- (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
+lemma "\<turnstile> (\<exists>x. P(x) \<longrightarrow> Q) \<longleftrightarrow> (\<forall>x. P(x)) \<longrightarrow> Q"
   by fast
 
-lemma "|- (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
+lemma "\<turnstile> (\<forall>x. P(x)) \<or> Q \<longleftrightarrow> (\<forall>x. P(x) \<or> Q)"
   by fast
 
 
 text "Basic test of quantifier reasoning"
 
-lemma "|- (\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
+lemma "\<turnstile> (\<exists>y. \<forall>x. Q(x,y)) \<longrightarrow> (\<forall>x. \<exists>y. Q(x,y))"
   by fast
 
-lemma "|- (\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
+lemma "\<turnstile> (\<forall>x. Q(x)) \<longrightarrow> (\<exists>x. Q(x))"
   by fast
 
 
 text "The following are invalid!"
 
 (*INVALID*)
-lemma "|- (\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
+lemma "\<turnstile> (\<forall>x. \<exists>y. Q(x,y)) \<longrightarrow> (\<exists>y. \<forall>x. Q(x,y))"
   apply fast?
   apply (rule _)
   oops
 
 (*INVALID*)
-lemma "|- (\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
+lemma "\<turnstile> (\<exists>x. Q(x)) \<longrightarrow> (\<forall>x. Q(x))"
   apply fast?
   apply (rule _)
   oops
 
 (*INVALID*)
-schematic_goal "|- P(?a) \<longrightarrow> (\<forall>x. P(x))"
+schematic_goal "\<turnstile> P(?a) \<longrightarrow> (\<forall>x. P(x))"
   apply fast?
   apply (rule _)
   oops
 
 (*INVALID*)
-schematic_goal "|- (P(?a) \<longrightarrow> (\<forall>x. Q(x))) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> Q(x))"
+schematic_goal "\<turnstile> (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 "|- (\<forall>x. P(x) \<longrightarrow> Q(x)) \<and> (\<exists>x. P(x)) \<longrightarrow> (\<exists>x. Q(x))"
+lemma "\<turnstile> (\<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 \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
+lemma "\<turnstile> (P \<longrightarrow> (\<exists>x. Q(x))) \<and> P \<longrightarrow> (\<exists>x. Q(x))"
   by fast
 
 
 text "Solving for a Var"
 
-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)"
+schematic_goal "\<turnstile> (\<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 "|- (\<forall>x y. P(x) \<longrightarrow> Q(y)) \<longleftrightarrow> ((\<exists>x. P(x)) \<longrightarrow> (\<forall>y. Q(y)))"
+lemma "\<turnstile> (\<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 "|- (\<exists>x y. P(x) \<and> Q(x,y)) \<longleftrightarrow> (\<exists>x. P(x) \<and> (\<exists>y. Q(x,y)))"
+lemma "\<turnstile> (\<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 "|- (\<exists>y. \<forall>x. P(x) \<longrightarrow> Q(x,y)) \<longrightarrow> (\<forall>x. P(x) \<longrightarrow> (\<exists>y. Q(x,y)))"
+lemma "\<turnstile> (\<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 538100cc4399 -r 0a29a984a91b src/Sequents/LK0.thy
--- a/src/Sequents/LK0.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/LK0.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -32,7 +32,7 @@
   Ex           :: "('a \<Rightarrow> o) \<Rightarrow> o"   (binder "\<exists>" 10)
 
 syntax
- "_Trueprop"    :: "two_seqe" ("((_)/ |- (_))" [6,6] 5)
+ "_Trueprop"    :: "two_seqe" ("((_)/ \<turnstile> (_))" [6,6] 5)
 
 parse_translation \<open>[(@{syntax_const "_Trueprop"}, K (two_seq_tr @{const_syntax Trueprop}))]\<close>
 print_translation \<open>[(@{const_syntax Trueprop}, K (two_seq_tr' @{syntax_const "_Trueprop"}))]\<close>
@@ -45,34 +45,34 @@
 
   (*Structural rules: contraction, thinning, exchange [Soren Heilmann] *)
 
-  contRS: "$H |- $E, $S, $S, $F \<Longrightarrow> $H |- $E, $S, $F" and
-  contLS: "$H, $S, $S, $G |- $E \<Longrightarrow> $H, $S, $G |- $E" and
+  contRS: "$H \<turnstile> $E, $S, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and
+  contLS: "$H, $S, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $E" and
 
-  thinRS: "$H |- $E, $F \<Longrightarrow> $H |- $E, $S, $F" and
-  thinLS: "$H, $G |- $E \<Longrightarrow> $H, $S, $G |- $E" and
+  thinRS: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, $S, $F" and
+  thinLS: "$H, $G \<turnstile> $E \<Longrightarrow> $H, $S, $G \<turnstile> $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
+  exchRS: "$H \<turnstile> $E, $R, $S, $F \<Longrightarrow> $H \<turnstile> $E, $S, $R, $F" and
+  exchLS: "$H, $R, $S, $G \<turnstile> $E \<Longrightarrow> $H, $S, $R, $G \<turnstile> $E" and
 
-  cut:   "\<lbrakk>$H |- $E, P;  $H, P |- $E\<rbrakk> \<Longrightarrow> $H |- $E" and
+  cut:   "\<lbrakk>$H \<turnstile> $E, P;  $H, P \<turnstile> $E\<rbrakk> \<Longrightarrow> $H \<turnstile> $E" and
 
   (*Propositional rules*)
 
-  basic: "$H, P, $G |- $E, P, $F" and
+  basic: "$H, P, $G \<turnstile> $E, P, $F" 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
+  conjR: "\<lbrakk>$H\<turnstile> $E, P, $F;  $H\<turnstile> $E, Q, $F\<rbrakk> \<Longrightarrow> $H\<turnstile> $E, P \<and> Q, $F" and
+  conjL: "$H, P, Q, $G \<turnstile> $E \<Longrightarrow> $H, P \<and> Q, $G \<turnstile> $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
+  disjR: "$H \<turnstile> $E, P, Q, $F \<Longrightarrow> $H \<turnstile> $E, P \<or> Q, $F" and
+  disjL: "\<lbrakk>$H, P, $G \<turnstile> $E;  $H, Q, $G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<or> Q, $G \<turnstile> $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
+  impR:  "$H, P \<turnstile> $E, Q, $F \<Longrightarrow> $H \<turnstile> $E, P \<longrightarrow> Q, $F" and
+  impL:  "\<lbrakk>$H,$G \<turnstile> $E,P;  $H, Q, $G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<longrightarrow> Q, $G \<turnstile> $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
+  notR:  "$H, P \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, \<not> P, $F" and
+  notL:  "$H, $G \<turnstile> $E, P \<Longrightarrow> $H, \<not> P, $G \<turnstile> $E" and
 
-  FalseL: "$H, False, $G |- $E" and
+  FalseL: "$H, False, $G \<turnstile> $E" and
 
   True_def: "True \<equiv> False \<longrightarrow> False" and
   iff_def:  "P \<longleftrightarrow> Q \<equiv> (P \<longrightarrow> Q) \<and> (Q \<longrightarrow> P)"
@@ -80,27 +80,27 @@
 axiomatization where
   (*Quantifiers*)
 
-  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
+  allR:  "(\<And>x. $H \<turnstile> $E, P(x), $F) \<Longrightarrow> $H \<turnstile> $E, \<forall>x. P(x), $F" and
+  allL:  "$H, P(x), $G, \<forall>x. P(x) \<turnstile> $E \<Longrightarrow> $H, \<forall>x. P(x), $G \<turnstile> $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
+  exR:   "$H \<turnstile> $E, P(x), $F, \<exists>x. P(x) \<Longrightarrow> $H \<turnstile> $E, \<exists>x. P(x), $F" and
+  exL:   "(\<And>x. $H, P(x), $G \<turnstile> $E) \<Longrightarrow> $H, \<exists>x. P(x), $G \<turnstile> $E" and
 
   (*Equality*)
-  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)"
+  refl:  "$H \<turnstile> $E, a = a, $F" and
+  subst: "\<And>G H E. $H(a), $G(a) \<turnstile> $E(a) \<Longrightarrow> $H(b), a=b, $G(b) \<turnstile> $E(b)"
 
   (* Reflection *)
 
 axiomatization where
-  eq_reflection:  "|- x = y \<Longrightarrow> (x \<equiv> y)" and
-  iff_reflection: "|- P \<longleftrightarrow> Q \<Longrightarrow> (P \<equiv> Q)"
+  eq_reflection:  "\<turnstile> x = y \<Longrightarrow> (x \<equiv> y)" and
+  iff_reflection: "\<turnstile> P \<longleftrightarrow> Q \<Longrightarrow> (P \<equiv> Q)"
 
   (*Descriptions*)
 
 axiomatization where
-  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"
+  The: "\<lbrakk>$H \<turnstile> $E, P(a), $F;  \<And>x.$H, P(x) \<turnstile> $E, x=a, $F\<rbrakk> \<Longrightarrow>
+         $H \<turnstile> $E, P(THE x. P(x)), $F"
 
 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)"
@@ -110,26 +110,26 @@
 
 (*contraction*)
 
-lemma contR: "$H |- $E, P, P, $F \<Longrightarrow> $H |- $E, P, $F"
+lemma contR: "$H \<turnstile> $E, P, P, $F \<Longrightarrow> $H \<turnstile> $E, P, $F"
   by (rule contRS)
 
-lemma contL: "$H, P, P, $G |- $E \<Longrightarrow> $H, P, $G |- $E"
+lemma contL: "$H, P, P, $G \<turnstile> $E \<Longrightarrow> $H, P, $G \<turnstile> $E"
   by (rule contLS)
 
 (*thinning*)
 
-lemma thinR: "$H |- $E, $F \<Longrightarrow> $H |- $E, P, $F"
+lemma thinR: "$H \<turnstile> $E, $F \<Longrightarrow> $H \<turnstile> $E, P, $F"
   by (rule thinRS)
 
-lemma thinL: "$H, $G |- $E \<Longrightarrow> $H, P, $G |- $E"
+lemma thinL: "$H, $G \<turnstile> $E \<Longrightarrow> $H, P, $G \<turnstile> $E"
   by (rule thinLS)
 
 (*exchange*)
 
-lemma exchR: "$H |- $E, Q, P, $F \<Longrightarrow> $H |- $E, P, Q, $F"
+lemma exchR: "$H \<turnstile> $E, Q, P, $F \<Longrightarrow> $H \<turnstile> $E, P, Q, $F"
   by (rule exchRS)
 
-lemma exchL: "$H, Q, P, $G |- $E \<Longrightarrow> $H, P, Q, $G |- $E"
+lemma exchL: "$H, Q, P, $G \<turnstile> $E \<Longrightarrow> $H, P, Q, $G \<turnstile> $E"
   by (rule exchLS)
 
 ML \<open>
@@ -146,21 +146,21 @@
 
 
 (** If-and-only-if rules **)
-lemma iffR: "\<lbrakk>$H,P |- $E,Q,$F;  $H,Q |- $E,P,$F\<rbrakk> \<Longrightarrow> $H |- $E, P \<longleftrightarrow> Q, $F"
+lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F;  $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F"
   apply (unfold iff_def)
   apply (assumption | rule conjR impR)+
   done
 
-lemma iffL: "\<lbrakk>$H,$G |- $E,P,Q;  $H,Q,P,$G |- $E\<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G |- $E"
+lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q;  $H,Q,P,$G \<turnstile> $E\<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $E"
   apply (unfold iff_def)
   apply (assumption | rule conjL impL basic)+
   done
 
-lemma iff_refl: "$H |- $E, (P \<longleftrightarrow> P), $F"
+lemma iff_refl: "$H \<turnstile> $E, (P \<longleftrightarrow> P), $F"
   apply (rule iffR basic)+
   done
 
-lemma TrueR: "$H |- $E, True, $F"
+lemma TrueR: "$H \<turnstile> $E, True, $F"
   apply (unfold True_def)
   apply (rule impR)
   apply (rule basic)
@@ -168,9 +168,9 @@
 
 (*Descriptions*)
 lemma the_equality:
-  assumes p1: "$H |- $E, P(a), $F"
-    and p2: "\<And>x. $H, P(x) |- $E, x=a, $F"
-  shows "$H |- $E, (THE x. P(x)) = a, $F"
+  assumes p1: "$H \<turnstile> $E, P(a), $F"
+    and p2: "\<And>x. $H, P(x) \<turnstile> $E, x=a, $F"
+  shows "$H \<turnstile> $E, (THE x. P(x)) = a, $F"
   apply (rule cut)
    apply (rule_tac [2] p2)
   apply (rule The, rule thinR, rule exchRS, rule p1)
@@ -180,12 +180,12 @@
 
 (** Weakened quantifier rules.  Incomplete, they let the search terminate.**)
 
-lemma allL_thin: "$H, P(x), $G |- $E \<Longrightarrow> $H, \<forall>x. P(x), $G |- $E"
+lemma allL_thin: "$H, P(x), $G \<turnstile> $E \<Longrightarrow> $H, \<forall>x. P(x), $G \<turnstile> $E"
   apply (rule allL)
   apply (erule thinL)
   done
 
-lemma exR_thin: "$H |- $E, P(x), $F \<Longrightarrow> $H |- $E, \<exists>x. P(x), $F"
+lemma exR_thin: "$H \<turnstile> $E, P(x), $F \<Longrightarrow> $H \<turnstile> $E, \<exists>x. P(x), $F"
   apply (rule exR)
   apply (erule thinR)
   done
@@ -233,18 +233,18 @@
 
 
 lemma mp_R:
-  assumes major: "$H |- $E, $F, P \<longrightarrow> Q"
-    and minor: "$H |- $E, $F, P"
-  shows "$H |- $E, Q, $F"
+  assumes major: "$H \<turnstile> $E, $F, P \<longrightarrow> Q"
+    and minor: "$H \<turnstile> $E, $F, P"
+  shows "$H \<turnstile> $E, Q, $F"
   apply (rule thinRS [THEN cut], rule major)
   apply step
   apply (rule thinR, rule minor)
   done
 
 lemma mp_L:
-  assumes major: "$H, $G |- $E, P \<longrightarrow> Q"
-    and minor: "$H, $G, Q |- $E"
-  shows "$H, P, $G |- $E"
+  assumes major: "$H, $G \<turnstile> $E, P \<longrightarrow> Q"
+    and minor: "$H, $G, Q \<turnstile> $E"
+  shows "$H, P, $G \<turnstile> $E"
   apply (rule thinL [THEN cut], rule major)
   apply step
   apply (rule thinL, rule minor)
@@ -254,18 +254,18 @@
 (** Two rules to generate left- and right- rules from implications **)
 
 lemma R_of_imp:
-  assumes major: "|- P \<longrightarrow> Q"
-    and minor: "$H |- $E, $F, P"
-  shows "$H |- $E, Q, $F"
+  assumes major: "\<turnstile> P \<longrightarrow> Q"
+    and minor: "$H \<turnstile> $E, $F, P"
+  shows "$H \<turnstile> $E, Q, $F"
   apply (rule mp_R)
    apply (rule_tac [2] minor)
   apply (rule thinRS, rule major [THEN thinLS])
   done
 
 lemma L_of_imp:
-  assumes major: "|- P \<longrightarrow> Q"
-    and minor: "$H, $G, Q |- $E"
-  shows "$H, P, $G |- $E"
+  assumes major: "\<turnstile> P \<longrightarrow> Q"
+    and minor: "$H, $G, Q \<turnstile> $E"
+  shows "$H, P, $G \<turnstile> $E"
   apply (rule mp_L)
    apply (rule_tac [2] minor)
   apply (rule thinRS, rule major [THEN thinLS])
@@ -273,24 +273,24 @@
 
 (*Can be used to create implications in a subgoal*)
 lemma backwards_impR:
-  assumes prem: "$H, $G |- $E, $F, P \<longrightarrow> Q"
-  shows "$H, P, $G |- $E, Q, $F"
+  assumes prem: "$H, $G \<turnstile> $E, $F, P \<longrightarrow> Q"
+  shows "$H, P, $G \<turnstile> $E, Q, $F"
   apply (rule mp_L)
    apply (rule_tac [2] basic)
   apply (rule thinR, rule prem)
   done
 
-lemma conjunct1: "|-P \<and> Q \<Longrightarrow> |-P"
+lemma conjunct1: "\<turnstile>P \<and> Q \<Longrightarrow> \<turnstile>P"
   apply (erule thinR [THEN cut])
   apply fast
   done
 
-lemma conjunct2: "|-P \<and> Q \<Longrightarrow> |-Q"
+lemma conjunct2: "\<turnstile>P \<and> Q \<Longrightarrow> \<turnstile>Q"
   apply (erule thinR [THEN cut])
   apply fast
   done
 
-lemma spec: "|- (\<forall>x. P(x)) \<Longrightarrow> |- P(x)"
+lemma spec: "\<turnstile> (\<forall>x. P(x)) \<Longrightarrow> \<turnstile> P(x)"
   apply (erule thinR [THEN cut])
   apply fast
   done
@@ -298,10 +298,10 @@
 
 (** Equality **)
 
-lemma sym: "|- a = b \<longrightarrow> b = a"
+lemma sym: "\<turnstile> a = b \<longrightarrow> b = a"
   by (safe add!: subst)
 
-lemma trans: "|- a = b \<longrightarrow> b = c \<longrightarrow> a = c"
+lemma trans: "\<turnstile> a = b \<longrightarrow> b = c \<longrightarrow> a = c"
   by (safe add!: subst)
 
 (* Symmetry of equality in hypotheses *)
@@ -310,18 +310,18 @@
 (* Symmetry of equality in hypotheses *)
 lemmas symR = sym [THEN R_of_imp]
 
-lemma transR: "\<lbrakk>$H|- $E, $F, a = b;  $H|- $E, $F, b=c\<rbrakk> \<Longrightarrow> $H|- $E, a = c, $F"
+lemma transR: "\<lbrakk>$H\<turnstile> $E, $F, a = b;  $H\<turnstile> $E, $F, b=c\<rbrakk> \<Longrightarrow> $H\<turnstile> $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 \<equiv> B) \<Longrightarrow> |- A \<longleftrightarrow> B"
+lemma def_imp_iff: "(A \<equiv> B) \<Longrightarrow> \<turnstile> A \<longleftrightarrow> B"
   apply unfold
   apply (rule iff_refl)
   done
 
-lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> |- A = B"
+lemma meta_eq_to_obj_eq: "(A \<equiv> B) \<Longrightarrow> \<turnstile> A = B"
   apply unfold
   apply (rule refl)
   done
@@ -329,19 +329,19 @@
 
 (** if-then-else rules **)
 
-lemma if_True: "|- (if True then x else y) = x"
+lemma if_True: "\<turnstile> (if True then x else y) = x"
   unfolding If_def by fast
 
-lemma if_False: "|- (if False then x else y) = y"
+lemma if_False: "\<turnstile> (if False then x else y) = y"
   unfolding If_def by fast
 
-lemma if_P: "|- P \<Longrightarrow> |- (if P then x else y) = x"
+lemma if_P: "\<turnstile> P \<Longrightarrow> \<turnstile> (if P then x else y) = x"
   apply (unfold If_def)
   apply (erule thinR [THEN cut])
   apply fast
   done
 
-lemma if_not_P: "|- \<not> P \<Longrightarrow> |- (if P then x else y) = y"
+lemma if_not_P: "\<turnstile> \<not> P \<Longrightarrow> \<turnstile> (if P then x else y) = y"
   apply (unfold If_def)
   apply (erule thinR [THEN cut])
   apply fast
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/Modal0.thy
--- a/src/Sequents/Modal0.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/Modal0.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -43,12 +43,12 @@
 
 lemmas rewrite_rls = strimp_def streqv_def
 
-lemma iffR: "\<lbrakk>$H,P |- $E,Q,$F;  $H,Q |- $E,P,$F\<rbrakk> \<Longrightarrow> $H |- $E, P \<longleftrightarrow> Q, $F"
+lemma iffR: "\<lbrakk>$H,P \<turnstile> $E,Q,$F;  $H,Q \<turnstile> $E,P,$F\<rbrakk> \<Longrightarrow> $H \<turnstile> $E, P \<longleftrightarrow> Q, $F"
   apply (unfold iff_def)
   apply (assumption | rule conjR impR)+
   done
 
-lemma iffL: "\<lbrakk>$H,$G |- $E,P,Q;  $H,Q,P,$G |- $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G |- $E"
+lemma iffL: "\<lbrakk>$H,$G \<turnstile> $E,P,Q;  $H,Q,P,$G \<turnstile> $E \<rbrakk> \<Longrightarrow> $H, P \<longleftrightarrow> Q, $G \<turnstile> $E"
   apply (unfold iff_def)
   apply (assumption | rule conjL impL basic)+
   done
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/S4.thy
--- a/src/Sequents/S4.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/S4.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -23,13 +23,13 @@
 
   boxR:
    "\<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
+           $E'         \<turnstile> $F', P, $G'\<rbrakk> \<Longrightarrow> $E          \<turnstile> $F, []P, $G" and
+  boxL:     "$E,P,$F,[]P \<turnstile>         $G    \<Longrightarrow> $E, []P, $F \<turnstile>          $G" and
 
-  diaR:     "$E          |- $F,P,$G,<>P   \<Longrightarrow> $E          |- $F, <>P, $G" and
+  diaR:     "$E          \<turnstile> $F,P,$G,<>P   \<Longrightarrow> $E          \<turnstile> $F, <>P, $G" and
   diaL:
    "\<lbrakk>$E |L> $E';  $F |L> $F';  $G |R> $G';
-           $E', P, $F' |-         $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F |- $G"
+           $E', P, $F' \<turnstile>         $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F \<turnstile> $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 \<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 "\<turnstile> []P \<longrightarrow> P" by S4_solve
+lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S4_solve   (* normality*)
+lemma "\<turnstile> (P --< Q) \<longrightarrow> []P \<longrightarrow> []Q" by S4_solve
+lemma "\<turnstile> P \<longrightarrow> <>P" 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 "\<turnstile>  [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve
+lemma "\<turnstile>  <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve
+lemma "\<turnstile>  [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >-< Q)" by S4_solve
+lemma "\<turnstile>  <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S4_solve
+lemma "\<turnstile>        []P \<longleftrightarrow> \<not> <>(\<not> P)" by S4_solve
+lemma "\<turnstile>     [](\<not> P) \<longleftrightarrow> \<not> <>P" by S4_solve
+lemma "\<turnstile>       \<not> []P \<longleftrightarrow> <>(\<not> P)" by S4_solve
+lemma "\<turnstile>      [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S4_solve
+lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>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
+lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve
+lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S4_solve
+lemma "\<turnstile> (P --< Q) \<and> (Q --< R) \<longrightarrow> (P --< R)" by S4_solve
+lemma "\<turnstile> []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
 
 
 (* Theorems of system S4 from Hughes and Cresswell, p.46 *)
 
-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
+lemma "\<turnstile> []A \<longrightarrow> A" by S4_solve             (* refexivity *)
+lemma "\<turnstile> []A \<longrightarrow> [][]A" by S4_solve         (* transitivity *)
+lemma "\<turnstile> []A \<longrightarrow> <>A" by S4_solve           (* seriality *)
+lemma "\<turnstile> <>[](<>A \<longrightarrow> []<>A)" by S4_solve
+lemma "\<turnstile> <>[](<>[]A \<longrightarrow> []A)" by S4_solve
+lemma "\<turnstile> []P \<longleftrightarrow> [][]P" by S4_solve
+lemma "\<turnstile> <>P \<longleftrightarrow> <><>P" by S4_solve
+lemma "\<turnstile> <>[]<>P \<longrightarrow> <>P" by S4_solve
+lemma "\<turnstile> []<>P \<longleftrightarrow> []<>[]<>P" by S4_solve
+lemma "\<turnstile> <>[]P \<longleftrightarrow> <>[]<>[]P" by S4_solve
 
 (* Theorems for system S4 from Hughes and Cresswell, p.60 *)
 
-lemma "|- []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S4_solve
-lemma "|- ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S4_solve
+lemma "\<turnstile> []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S4_solve
+lemma "\<turnstile> ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S4_solve
 
 (* These are from Hailpern, LNCS 129 *)
 
-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 "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S4_solve
+lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S4_solve
+lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" 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 "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S4_solve
+lemma "\<turnstile> []P \<longrightarrow> []<>P" by S4_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> <>P" 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 "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S4_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S4_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S4_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S4_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S4_solve
 
 end
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/S43.thy
--- a/src/Sequents/S43.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/S43.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -48,32 +48,32 @@
 (* ie                                                                        *)
 (*           S1...Sk,Sk+1...Sk+m                                             *)
 (*     ----------------------------------                                    *)
-(*     <>P1...<>Pk, $G |- $H, []Q1...[]Qm                                    *)
+(*     <>P1...<>Pk, $G \<turnstile> $H, []Q1...[]Qm                                    *)
 (*                                                                           *)
-(*  where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * |- $H *, []Q1...[]Qm    *)
-(*    and Sj == <>P1...<>Pk, $G * |- $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
+(*  where Si == <>P1...<>Pi-1,<>Pi+1,..<>Pk,Pi, $G * \<turnstile> $H *, []Q1...[]Qm    *)
+(*    and Sj == <>P1...<>Pk, $G * \<turnstile> $H *, []Q1...[]Qj-1,[]Qj+1...[]Qm,Qj    *)
 (*    and 1<=i<=k and k<j<=k+m                                               *)
 
   S43pi0:         "S43pi $L;; $R;; $Lbox; $Rdia" and
   S43pi1:
-   "\<lbrakk>(S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox |- $R,$Rdia\<rbrakk> \<Longrightarrow>
+   "\<lbrakk>(S43pi <>P,$L';     $L;; $R; $Lbox;$Rdia);   $L',P,$L,$Lbox \<turnstile> $R,$Rdia\<rbrakk> \<Longrightarrow>
        S43pi     $L'; <>P,$L;; $R; $Lbox;$Rdia" and
   S43pi2:
-   "\<lbrakk>(S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox |- $R',P,$R,$Rdia\<rbrakk> \<Longrightarrow>
+   "\<lbrakk>(S43pi $L';; []P,$R';     $R; $Lbox;$Rdia);  $L',$Lbox \<turnstile> $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 \<Longrightarrow> $E, []P, $F |- $G" and
-  diaR:           "$E |- $F, P, $G, <>P \<Longrightarrow> $E |- $F, <>P, $G" and
+  boxL:           "$E, P, $F, []P \<turnstile> $G \<Longrightarrow> $E, []P, $F \<turnstile> $G" and
+  diaR:           "$E \<turnstile> $F, P, $G, <>P \<Longrightarrow> $E \<turnstile> $F, <>P, $G" and
   pi1:
    "\<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
+   $L1, <>P, $L2 \<turnstile> $R" and
   pi2:
    "\<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"
+   $L \<turnstile> $R1, []P, $R2"
 
 
 ML \<open>
@@ -97,108 +97,108 @@
 
 (* Theorems of system T from Hughes and Cresswell and Hailpern, LNCS 129 *)
 
-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 "\<turnstile> []P \<longrightarrow> P" by S43_solve
+lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by S43_solve   (* normality*)
+lemma "\<turnstile> (P--<Q) \<longrightarrow> []P \<longrightarrow> []Q" by S43_solve
+lemma "\<turnstile> P \<longrightarrow> <>P" 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 "\<turnstile>  [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "\<turnstile>  <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "\<turnstile>  [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P>-<Q)" by S43_solve
+lemma "\<turnstile>  <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by S43_solve
+lemma "\<turnstile>        []P \<longleftrightarrow> \<not> <>(\<not> P)" by S43_solve
+lemma "\<turnstile>     [](\<not>P) \<longleftrightarrow> \<not> <>P" by S43_solve
+lemma "\<turnstile>       \<not> []P \<longleftrightarrow> <>(\<not> P)" by S43_solve
+lemma "\<turnstile>      [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by S43_solve
+lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>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
+lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
+lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by S43_solve
+lemma "\<turnstile> (P --< Q) \<and> (Q --<R ) \<longrightarrow> (P --< R)" by S43_solve
+lemma "\<turnstile> []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
 
 
 (* Theorems of system S4 from Hughes and Cresswell, p.46 *)
 
-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
+lemma "\<turnstile> []A \<longrightarrow> A" by S43_solve             (* refexivity *)
+lemma "\<turnstile> []A \<longrightarrow> [][]A" by S43_solve         (* transitivity *)
+lemma "\<turnstile> []A \<longrightarrow> <>A" by S43_solve           (* seriality *)
+lemma "\<turnstile> <>[](<>A \<longrightarrow> []<>A)" by S43_solve
+lemma "\<turnstile> <>[](<>[]A \<longrightarrow> []A)" by S43_solve
+lemma "\<turnstile> []P \<longleftrightarrow> [][]P" by S43_solve
+lemma "\<turnstile> <>P \<longleftrightarrow> <><>P" by S43_solve
+lemma "\<turnstile> <>[]<>P \<longrightarrow> <>P" by S43_solve
+lemma "\<turnstile> []<>P \<longleftrightarrow> []<>[]<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longleftrightarrow> <>[]<>[]P" by S43_solve
 
 (* Theorems for system S4 from Hughes and Cresswell, p.60 *)
 
-lemma "|- []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S43_solve
-lemma "|- ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S43_solve
+lemma "\<turnstile> []P \<or> []Q \<longleftrightarrow> []([]P \<or> []Q)" by S43_solve
+lemma "\<turnstile> ((P >-< Q) --< R) \<longrightarrow> ((P >-< Q) --< []R)" by S43_solve
 
 (* These are from Hailpern, LNCS 129 *)
 
-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 "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" 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 "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> (<>P \<longrightarrow> <>Q)" by S43_solve
+lemma "\<turnstile> []P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> <>[]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 \<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 "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
 
 
 (* Theorems of system S43 *)
 
-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
+lemma "\<turnstile> <>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> [][]<>P" by S43_solve
+lemma "\<turnstile> [](<>P \<or> <>Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
+lemma "\<turnstile> <>[]P \<and> <>[]Q \<longrightarrow> <>([]P \<and> []Q)" by S43_solve
+lemma "\<turnstile> []([]P \<longrightarrow> []Q) \<or> []([]Q \<longrightarrow> []P)" by S43_solve
+lemma "\<turnstile> [](<>P \<longrightarrow> <>Q) \<or> [](<>Q \<longrightarrow> <>P)" by S43_solve
+lemma "\<turnstile> []([]P \<longrightarrow> Q) \<or> []([]Q \<longrightarrow> P)" by S43_solve
+lemma "\<turnstile> [](P \<longrightarrow> <>Q) \<or> [](Q \<longrightarrow> <>P)" by S43_solve
+lemma "\<turnstile> [](P \<longrightarrow> []Q \<longrightarrow> R) \<or> [](P \<or> ([]R \<longrightarrow> Q))" by S43_solve
+lemma "\<turnstile> [](P \<or> (Q \<longrightarrow> <>C)) \<or> [](P \<longrightarrow> C \<longrightarrow> <>Q)" by S43_solve
+lemma "\<turnstile> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
+lemma "\<turnstile> <>P \<and> <>Q \<longrightarrow> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<and> []([]P \<or> Q) \<and> [](P \<or> []Q) \<longrightarrow> []P \<or> []Q" by S43_solve
+lemma "\<turnstile> <>P \<and> <>Q \<longrightarrow> <>(P \<and> Q) \<or> <>(<>P \<and> Q) \<or> <>(P \<and> <>Q)" by S43_solve
+lemma "\<turnstile> <>[]<>P \<longleftrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
 
 (* These are from Hailpern, LNCS 129 *)
 
-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 "\<turnstile> [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by S43_solve
+lemma "\<turnstile> <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>(P \<longrightarrow> Q) \<longleftrightarrow> []P \<longrightarrow> <>Q" 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 "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> <>P \<longrightarrow> <>Q" by S43_solve
+lemma "\<turnstile> []P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> <>P" by S43_solve
+lemma "\<turnstile> []<>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> <>[]<>P" by S43_solve
+lemma "\<turnstile> <>[]P \<longrightarrow> []<>P" by S43_solve
+lemma "\<turnstile> []<>[]P \<longleftrightarrow> <>[]P" by S43_solve
+lemma "\<turnstile> <>[]<>P \<longleftrightarrow> []<>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 \<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
+lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by S43_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by S43_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by S43_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []<>P \<or> []<>Q" by S43_solve
+lemma "\<turnstile> <>[]P \<and> <>[]Q \<longrightarrow> <>(P \<and> Q)" by S43_solve
+lemma "\<turnstile> <>[](P \<and> Q) \<longleftrightarrow> <>[]P \<and> <>[]Q" by S43_solve
+lemma "\<turnstile> []<>(P \<or> Q) \<longleftrightarrow> []<>P \<or> []<>Q" by S43_solve
 
 end
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/Sequents.thy
--- a/src/Sequents/Sequents.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/Sequents.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -21,8 +21,8 @@
 
 typedecl seq'
 consts
- SeqO'         :: "[o,seq']=>seq'"
- Seq1'         :: "o=>seq'"
+ SeqO'         :: "[o,seq']\<Rightarrow>seq'"
+ Seq1'         :: "o\<Rightarrow>seq'"
 
 
 subsection \<open>Concrete syntax\<close>
@@ -31,28 +31,28 @@
 
 syntax
  "_SeqEmp"         :: seq                                  ("")
- "_SeqApp"         :: "[seqobj,seqcont] => seq"            ("__")
+ "_SeqApp"         :: "[seqobj,seqcont] \<Rightarrow> seq"            ("__")
 
  "_SeqContEmp"     :: seqcont                              ("")
- "_SeqContApp"     :: "[seqobj,seqcont] => seqcont"        (",/ __")
+ "_SeqContApp"     :: "[seqobj,seqcont] \<Rightarrow> seqcont"        (",/ __")
 
- "_SeqO"           :: "o => seqobj"                        ("_")
- "_SeqId"          :: "'a => seqobj"                       ("$_")
+ "_SeqO"           :: "o \<Rightarrow> seqobj"                        ("_")
+ "_SeqId"          :: "'a \<Rightarrow> seqobj"                       ("$_")
 
-type_synonym single_seqe = "[seq,seqobj] => prop"
-type_synonym single_seqi = "[seq'=>seq',seq'=>seq'] => prop"
-type_synonym two_seqi = "[seq'=>seq', seq'=>seq'] => prop"
-type_synonym two_seqe = "[seq, seq] => prop"
-type_synonym three_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
-type_synonym three_seqe = "[seq, seq, seq] => prop"
-type_synonym four_seqi = "[seq'=>seq', seq'=>seq', seq'=>seq', seq'=>seq'] => prop"
-type_synonym four_seqe = "[seq, seq, seq, seq] => prop"
-type_synonym sequence_name = "seq'=>seq'"
+type_synonym single_seqe = "[seq,seqobj] \<Rightarrow> prop"
+type_synonym single_seqi = "[seq'\<Rightarrow>seq',seq'\<Rightarrow>seq'] \<Rightarrow> prop"
+type_synonym two_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
+type_synonym two_seqe = "[seq, seq] \<Rightarrow> prop"
+type_synonym three_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
+type_synonym three_seqe = "[seq, seq, seq] \<Rightarrow> prop"
+type_synonym four_seqi = "[seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq', seq'\<Rightarrow>seq'] \<Rightarrow> prop"
+type_synonym four_seqe = "[seq, seq, seq, seq] \<Rightarrow> prop"
+type_synonym sequence_name = "seq'\<Rightarrow>seq'"
 
 
 syntax
   (*Constant to allow definitions of SEQUENCES of formulas*)
-  "_Side"        :: "seq=>(seq'=>seq')"     ("<<(_)>>")
+  "_Side"        :: "seq\<Rightarrow>(seq'\<Rightarrow>seq')"     ("<<(_)>>")
 
 ML \<open>
 
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/T.thy
--- a/src/Sequents/T.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/T.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -23,12 +23,12 @@
 
   boxR:
    "\<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
+               $E'        \<turnstile> $F', P, $G'\<rbrakk> \<Longrightarrow> $E          \<turnstile> $F, []P, $G" and
+  boxL:     "$E, P, $F  \<turnstile>         $G    \<Longrightarrow> $E, []P, $F \<turnstile>          $G" and
+  diaR:     "$E         \<turnstile> $F, P,  $G    \<Longrightarrow> $E          \<turnstile> $F, <>P, $G" and
   diaL:
    "\<lbrakk>$E |L> $E';  $F |L> $F';  $G |R> $G';
-               $E', P, $F'|-         $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F |-          $G"
+               $E', P, $F'\<turnstile>         $G'\<rbrakk> \<Longrightarrow> $E, <>P, $F \<turnstile>          $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 \<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 "\<turnstile> []P \<longrightarrow> P" by T_solve
+lemma "\<turnstile> [](P \<longrightarrow> Q) \<longrightarrow> ([]P \<longrightarrow> []Q)" by T_solve   (* normality*)
+lemma "\<turnstile> (P --< Q) \<longrightarrow> []P \<longrightarrow> []Q" by T_solve
+lemma "\<turnstile> P \<longrightarrow> <>P" 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 "\<turnstile>  [](P \<and> Q) \<longleftrightarrow> []P \<and> []Q" by T_solve
+lemma "\<turnstile>  <>(P \<or> Q) \<longleftrightarrow> <>P \<or> <>Q" by T_solve
+lemma "\<turnstile>  [](P \<longleftrightarrow> Q) \<longleftrightarrow> (P >-< Q)" by T_solve
+lemma "\<turnstile>  <>(P \<longrightarrow> Q) \<longleftrightarrow> ([]P \<longrightarrow> <>Q)" by T_solve
+lemma "\<turnstile>        []P \<longleftrightarrow> \<not> <>(\<not> P)" by T_solve
+lemma "\<turnstile>     [](\<not> P) \<longleftrightarrow> \<not> <>P" by T_solve
+lemma "\<turnstile>       \<not> []P \<longleftrightarrow> <>(\<not> P)" by T_solve
+lemma "\<turnstile>      [][]P \<longleftrightarrow> \<not> <><>(\<not> P)" by T_solve
+lemma "\<turnstile> \<not> <>(P \<or> Q) \<longleftrightarrow> \<not> <>P \<and> \<not> <>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
+lemma "\<turnstile> []P \<or> []Q \<longrightarrow> [](P \<or> Q)" by T_solve
+lemma "\<turnstile> <>(P \<and> Q) \<longrightarrow> <>P \<and> <>Q" by T_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> []P \<or> <>Q" by T_solve
+lemma "\<turnstile> <>P \<and> []Q \<longrightarrow> <>(P \<and> Q)" by T_solve
+lemma "\<turnstile> [](P \<or> Q) \<longrightarrow> <>P \<or> []Q" by T_solve
+lemma "\<turnstile> <>(P \<longrightarrow> (Q \<and> R)) \<longrightarrow> ([]P \<longrightarrow> <>Q) \<and> ([]P \<longrightarrow> <>R)" by T_solve
+lemma "\<turnstile> (P --< Q) \<and> (Q --< R ) \<longrightarrow> (P --< R)" by T_solve
+lemma "\<turnstile> []P \<longrightarrow> <>Q \<longrightarrow> <>(P \<and> Q)" by T_solve
 
 end
diff -r 538100cc4399 -r 0a29a984a91b src/Sequents/Washing.thy
--- a/src/Sequents/Washing.thy	Sat Oct 10 20:51:39 2015 +0200
+++ b/src/Sequents/Washing.thy	Sat Oct 10 20:54:44 2015 +0200
@@ -15,19 +15,19 @@
   clean :: o
 where
   change:
-  "dollar |- (quarter >< quarter >< quarter >< quarter)" and
+  "dollar \<turnstile> (quarter >< quarter >< quarter >< quarter)" and
 
   load1:
-  "quarter , quarter , quarter , quarter , quarter |- loaded" and
+  "quarter , quarter , quarter , quarter , quarter \<turnstile> loaded" and
 
   load2:
-  "dollar , quarter |- loaded" and
+  "dollar , quarter \<turnstile> loaded" and
 
   wash:
-  "loaded , dirty |- wet" and
+  "loaded , dirty \<turnstile> wet" and
 
   dry:
-  "wet, quarter , quarter , quarter |- clean"
+  "wet, quarter , quarter , quarter \<turnstile> clean"
 
 
 (* "activate" definitions for use in proof *)
@@ -39,17 +39,17 @@
 
 (* a load of dirty clothes and two dollars gives you clean clothes *)
 
-lemma "dollar , dollar , dirty |- clean"
+lemma "dollar , dollar , dirty \<turnstile> clean"
   by (best add!: changeI load1I washI dryI)
 
 (* order of premises doesn't matter *)
 
-lemma "dollar , dirty , dollar |- clean"
+lemma "dollar , dirty , dollar \<turnstile> clean"
   by (best add!: changeI load1I washI dryI)
 
 (* alternative formulation *)
 
-lemma "dollar , dollar |- dirty -o clean"
+lemma "dollar , dollar \<turnstile> dirty -o clean"
   by (best add!: changeI load1I washI dryI)
 
 end