# HG changeset patch
# User wenzelm
# Date 1451508720 -3600
# Node ID 8cba509ace9cd38edc630d320e1a5c78afdddc70
# Parent  89291b5d0ede5c7e3e385787a2f110467363bd9a
more symbols;

diff -r 89291b5d0ede -r 8cba509ace9c src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Dec 30 21:52:00 2015 +0100
@@ -30,17 +30,17 @@
   "weakeningIOA A C h = (!ex. ex : executions C --> cex_abs h ex : executions A)"
 definition
   temp_strengthening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where
-  "temp_strengthening Q P h = (!ex. (cex_abs h ex |== Q) --> (ex |== P))"
+  "temp_strengthening Q P h = (!ex. (cex_abs h ex \<TTurnstile> Q) --> (ex \<TTurnstile> P))"
 definition
   temp_weakening :: "('a,'s2)ioa_temp => ('a,'s1)ioa_temp => ('s1 => 's2) => bool" where
-  "temp_weakening Q P h = temp_strengthening (.~ Q) (.~ P) h"
+  "temp_weakening Q P h = temp_strengthening (\<^bold>\<not> Q) (\<^bold>\<not> P) h"
 
 definition
   state_strengthening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where
   "state_strengthening Q P h = (!s t a.  Q (h(s),a,h(t)) --> P (s,a,t))"
 definition
   state_weakening :: "('a,'s2)step_pred => ('a,'s1)step_pred => ('s1 => 's2) => bool" where
-  "state_weakening Q P h = state_strengthening (.~Q) (.~P) h"
+  "state_weakening Q P h = state_strengthening (\<^bold>\<not>Q) (\<^bold>\<not>P) h"
 
 definition
   is_live_abstraction :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
@@ -83,7 +83,7 @@
 
 subsection "lemmas"
 
-lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex |== P) --> (cex_abs h ex |== Q))"
+lemma temp_weakening_def2: "temp_weakening Q P h = (! ex. (ex \<TTurnstile> P) --> (cex_abs h ex \<TTurnstile> Q))"
   apply (simp add: temp_weakening_def temp_strengthening_def NOT_def temp_sat_def satisfies_def)
   apply auto
   done
@@ -131,16 +131,16 @@
 
 (* FIX: Nach TLS.ML *)
 
-lemma IMPLIES_temp_sat: "(ex |== P .--> Q) = ((ex |== P) --> (ex |== Q))"
+lemma IMPLIES_temp_sat: "(ex \<TTurnstile> P \<^bold>\<longrightarrow> Q) = ((ex \<TTurnstile> P) --> (ex \<TTurnstile> Q))"
   by (simp add: IMPLIES_def temp_sat_def satisfies_def)
 
-lemma AND_temp_sat: "(ex |== P .& Q) = ((ex |== P) & (ex |== Q))"
+lemma AND_temp_sat: "(ex \<TTurnstile> P \<^bold>\<and> Q) = ((ex \<TTurnstile> P) & (ex \<TTurnstile> Q))"
   by (simp add: AND_def temp_sat_def satisfies_def)
 
-lemma OR_temp_sat: "(ex |== P .| Q) = ((ex |== P) | (ex |== Q))"
+lemma OR_temp_sat: "(ex \<TTurnstile> P \<^bold>\<or> Q) = ((ex \<TTurnstile> P) | (ex \<TTurnstile> Q))"
   by (simp add: OR_def temp_sat_def satisfies_def)
 
-lemma NOT_temp_sat: "(ex |== .~ P) = (~ (ex |== P))"
+lemma NOT_temp_sat: "(ex \<TTurnstile> \<^bold>\<not> P) = (~ (ex \<TTurnstile> P))"
   by (simp add: NOT_def temp_sat_def satisfies_def)
 
 declare IMPLIES_temp_sat [simp] AND_temp_sat [simp] OR_temp_sat [simp] NOT_temp_sat [simp]
@@ -160,7 +160,7 @@
 
 lemma AbsRuleTImprove:
    "[|is_live_abstraction h (C,L) (A,M);
-          validLIOA (A,M) (H1 .--> Q);  temp_strengthening Q P h;
+          validLIOA (A,M) (H1 \<^bold>\<longrightarrow> Q);  temp_strengthening Q P h;
           temp_weakening H1 H2 h; validLIOA (C,L) H2 |]
           ==> validLIOA (C,L) P"
 apply (unfold is_live_abstraction_def)
@@ -287,7 +287,7 @@
 lemma strength_AND:
 "[| temp_strengthening P1 Q1 h;
           temp_strengthening P2 Q2 h |]
-       ==> temp_strengthening (P1 .& P2) (Q1 .& Q2) h"
+       ==> temp_strengthening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
 apply (unfold temp_strengthening_def)
 apply auto
 done
@@ -295,14 +295,14 @@
 lemma strength_OR:
 "[| temp_strengthening P1 Q1 h;
           temp_strengthening P2 Q2 h |]
-       ==> temp_strengthening (P1 .| P2) (Q1 .| Q2) h"
+       ==> temp_strengthening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
 apply (unfold temp_strengthening_def)
 apply auto
 done
 
 lemma strength_NOT:
 "[| temp_weakening P Q h |]
-       ==> temp_strengthening (.~ P) (.~ Q) h"
+       ==> temp_strengthening (\<^bold>\<not> P) (\<^bold>\<not> Q) h"
 apply (unfold temp_strengthening_def)
 apply (simp add: temp_weakening_def2)
 apply auto
@@ -311,7 +311,7 @@
 lemma strength_IMPLIES:
 "[| temp_weakening P1 Q1 h;
           temp_strengthening P2 Q2 h |]
-       ==> temp_strengthening (P1 .--> P2) (Q1 .--> Q2) h"
+       ==> temp_strengthening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h"
 apply (unfold temp_strengthening_def)
 apply (simp add: temp_weakening_def2)
 done
@@ -320,20 +320,20 @@
 lemma weak_AND:
 "[| temp_weakening P1 Q1 h;
           temp_weakening P2 Q2 h |]
-       ==> temp_weakening (P1 .& P2) (Q1 .& Q2) h"
+       ==> temp_weakening (P1 \<^bold>\<and> P2) (Q1 \<^bold>\<and> Q2) h"
 apply (simp add: temp_weakening_def2)
 done
 
 lemma weak_OR:
 "[| temp_weakening P1 Q1 h;
           temp_weakening P2 Q2 h |]
-       ==> temp_weakening (P1 .| P2) (Q1 .| Q2) h"
+       ==> temp_weakening (P1 \<^bold>\<or> P2) (Q1 \<^bold>\<or> Q2) h"
 apply (simp add: temp_weakening_def2)
 done
 
 lemma weak_NOT:
 "[| temp_strengthening P Q h |]
-       ==> temp_weakening (.~ P) (.~ Q) h"
+       ==> temp_weakening (\<^bold>\<not> P) (\<^bold>\<not> Q) h"
 apply (unfold temp_strengthening_def)
 apply (simp add: temp_weakening_def2)
 apply auto
@@ -342,7 +342,7 @@
 lemma weak_IMPLIES:
 "[| temp_strengthening P1 Q1 h;
           temp_weakening P2 Q2 h |]
-       ==> temp_weakening (P1 .--> P2) (Q1 .--> Q2) h"
+       ==> temp_weakening (P1 \<^bold>\<longrightarrow> P2) (Q1 \<^bold>\<longrightarrow> Q2) h"
 apply (unfold temp_strengthening_def)
 apply (simp add: temp_weakening_def2)
 done
diff -r 89291b5d0ede -r 8cba509ace9c src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Dec 30 21:52:00 2015 +0100
@@ -15,18 +15,18 @@
 
 definition
   validLIOA :: "('a,'s)live_ioa => ('a,'s)ioa_temp  => bool" where
-  "validLIOA AL P = validIOA (fst AL) ((snd AL) .--> P)"
+  "validLIOA AL P = validIOA (fst AL) ((snd AL) \<^bold>\<longrightarrow> P)"
 
 definition
   WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
-  "WF A acts = (\<diamond>\<box><%(s,a,t) . Enabled A acts s> .--> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
+  "WF A acts = (\<diamond>\<box><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
 definition
   SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
-  "SF A acts = (\<box>\<diamond><%(s,a,t) . Enabled A acts s> .--> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
+  "SF A acts = (\<box>\<diamond><%(s,a,t) . Enabled A acts s> \<^bold>\<longrightarrow> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
 
 definition
   liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
-  "liveexecutions AP = {exec. exec : executions (fst AP) & (exec |== (snd AP))}"
+  "liveexecutions AP = {exec. exec : executions (fst AP) & (exec \<TTurnstile> (snd AP))}"
 definition
   livetraces :: "('a,'s)live_ioa => 'a trace set" where
   "livetraces AP = {mk_trace (fst AP)$(snd ex) | ex. ex:liveexecutions AP}"
@@ -39,8 +39,8 @@
   is_live_ref_map :: "('s1 => 's2) => ('a,'s1)live_ioa => ('a,'s2)live_ioa => bool" where
   "is_live_ref_map f CL AM =
            (is_ref_map f (fst CL ) (fst AM) &
-            (! exec : executions (fst CL). (exec |== (snd CL)) -->
-                                           ((corresp_ex (fst AM) f exec) |== (snd AM))))"
+            (! exec : executions (fst CL). (exec \<TTurnstile> (snd CL)) -->
+                                           ((corresp_ex (fst AM) f exec) \<TTurnstile> (snd AM))))"
 
 
 lemma live_implements_trans:
diff -r 89291b5d0ede -r 8cba509ace9c src/HOL/HOLCF/IOA/meta_theory/Pred.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Pred.thy	Wed Dec 30 21:52:00 2015 +0100
@@ -15,50 +15,33 @@
 
 consts
 
-satisfies    ::"'a  => 'a predicate => bool"    ("_ |= _" [100,9] 8)
+satisfies    ::"'a  => 'a predicate => bool"    ("_ \<Turnstile> _" [100,9] 8)
 valid        ::"'a predicate => bool"           (*  ("|-") *)
 
-NOT          ::"'a predicate => 'a predicate"  (".~ _" [40] 40)
-AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".&" 35)
-OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".|" 30)
-IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr ".-->" 25)
-
-
-notation (output)
-  NOT  ("~ _" [40] 40) and
-  AND  (infixr "&" 35) and
-  OR  (infixr "|" 30) and
-  IMPLIES  (infixr "-->" 25)
-
-notation (xsymbols output)
-  NOT  ("\<not> _" [40] 40) and
-  AND  (infixr "\<and>" 35) and
-  OR  (infixr "\<or>" 30) and
-  IMPLIES  (infixr "\<longrightarrow>" 25)
-
-notation (xsymbols)
-  satisfies  ("_ \<Turnstile> _" [100,9] 8)
+NOT          ::"'a predicate => 'a predicate"  ("\<^bold>\<not> _" [40] 40)
+AND          ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<^bold>\<and>" 35)
+OR           ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<^bold>\<or>" 30)
+IMPLIES      ::"'a predicate => 'a predicate => 'a predicate"    (infixr "\<^bold>\<longrightarrow>" 25)
 
 
 defs
 
 satisfies_def:
-   "s |= P  == P s"
+   "s \<Turnstile> P  == P s"
 
-(* priority einfuegen, da clash mit |=, wenn graphisches Symbol *)
 valid_def:
-   "valid P == (! s. (s |= P))"
+   "valid P == (! s. (s \<Turnstile> P))"
 
 NOT_def:
   "NOT P s ==  ~ (P s)"
 
 AND_def:
-  "(P .& Q) s == (P s) & (Q s)"
+  "(P \<^bold>\<and> Q) s == (P s) & (Q s)"
 
 OR_def:
-  "(P .| Q) s ==  (P s) | (Q s)"
+  "(P \<^bold>\<or> Q) s ==  (P s) | (Q s)"
 
 IMPLIES_def:
-  "(P .--> Q) s == (P s) --> (Q s)"
+  "(P \<^bold>\<longrightarrow> Q) s == (P s) --> (Q s)"
 
 end
diff -r 89291b5d0ede -r 8cba509ace9c src/HOL/HOLCF/IOA/meta_theory/Sequence.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Sequence.thy	Wed Dec 30 21:52:00 2015 +0100
@@ -792,7 +792,7 @@
 
 lemma divide_Seq_lemma:
  "HD$(Filter P$y) = Def x
-    --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y))) 
+    --> y = ((Takewhile (%x. ~P x)$y) @@ (x >> TL$(Dropwhile (%a. ~P a)$y)))
              & Finite (Takewhile (%x. ~ P x)$y)  & P x"
 
 (* FIX: pay attention: is only admissible with chain-finite package to be added to
@@ -809,7 +809,7 @@
 done
 
 lemma divide_Seq: "(x>>xs) << Filter P$y 
-   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a.~P a)$y)))
+   ==> y = ((Takewhile (%a. ~ P a)$y) @@ (x >> TL$(Dropwhile (%a. ~ P a)$y)))
       & Finite (Takewhile (%a. ~ P a)$y)  & P x"
 apply (rule divide_Seq_lemma [THEN mp])
 apply (drule_tac f="HD" and x="x>>xs" in  monofun_cfun_arg)
@@ -1030,7 +1030,7 @@
 
 (* In general: How to do this case without the same adm problems
    as for the entire proof ? *)
-lemma Filter_lemma1: "Forall (%x.~(P x & Q x)) s
+lemma Filter_lemma1: "Forall (%x. ~(P x & Q x)) s
           --> Filter P$(Filter Q$s) =
               Filter (%x. P x & Q x)$s"
 
@@ -1054,7 +1054,7 @@
 
 lemma FilterPQ_takelemma: "Filter P$(Filter Q$s) = Filter (%x. P x & Q x)$s"
 apply (rule_tac A1="%x. True" and
-                 Q1="%x.~(P x & Q x)" and x1="s" in
+                 Q1="%x. ~(P x & Q x)" and x1="s" in
                  take_lemma_induct [THEN mp])
 (* better support for A = %x. True *)
 apply (simp add: Filter_lemma1)
diff -r 89291b5d0ede -r 8cba509ace9c src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/ShortExecutions.thy	Wed Dec 30 21:52:00 2015 +0100
@@ -20,8 +20,8 @@
     | x##xs =>
       (case x of
         UU => UU
-      | Def y => (Takewhile (%x.~P x)$s)
-                  @@ (y>>(h$(TL$(Dropwhile (%x.~ P x)$s))$xs))
+      | Def y => (Takewhile (%x. \<not>P x)$s)
+                  @@ (y>>(h$(TL$(Dropwhile (%x. \<not> P x)$s))$xs))
       )
     ))"
 
@@ -64,8 +64,8 @@
     | x##xs =>
       (case x of
         UU => UU
-      | Def y => (Takewhile (%a.~ P a)$s)
-                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$xs))
+      | Def y => (Takewhile (%a. \<not> P a)$s)
+                  @@ (y>>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$xs))
       )
     )"
 apply (rule trans)
@@ -86,8 +86,8 @@
 done
 
 lemma oraclebuild_cons: "oraclebuild P$s$(x>>t) =
-          (Takewhile (%a.~ P a)$s)
-           @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a.~ P a)$s))$t))"
+          (Takewhile (%a. \<not> P a)$s)
+           @@ (x>>(oraclebuild P$(TL$(Dropwhile (%a. \<not> P a)$s))$t))"
 apply (rule trans)
 apply (subst oraclebuild_unfold)
 apply (simp add: Consq_def)
@@ -98,7 +98,7 @@
 subsection "Cut rewrite rules"
 
 lemma Cut_nil:
-"[| Forall (%a.~ P a) s; Finite s|]
+"[| Forall (%a. \<not> P a) s; Finite s|]
             ==> Cut P s =nil"
 apply (unfold Cut_def)
 apply (subgoal_tac "Filter P$s = nil")
@@ -108,7 +108,7 @@
 done
 
 lemma Cut_UU:
-"[| Forall (%a.~ P a) s; ~Finite s|]
+"[| Forall (%a. \<not> P a) s; ~Finite s|]
             ==> Cut P s =UU"
 apply (unfold Cut_def)
 apply (subgoal_tac "Filter P$s= UU")
@@ -118,7 +118,7 @@
 done
 
 lemma Cut_Cons:
-"[| P t;  Forall (%x.~ P x) ss; Finite ss|]
+"[| P t;  Forall (%x. \<not> P x) ss; Finite ss|]
             ==> Cut P (ss @@ (t>> rs))
                  = ss @@ (t >> Cut P rs)"
 apply (unfold Cut_def)
@@ -129,7 +129,7 @@
 subsection "Cut lemmas for main theorem"
 
 lemma FilterCut: "Filter P$s = Filter P$(Cut P s)"
-apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in take_lemma_induct [THEN mp])
+apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in take_lemma_induct [THEN mp])
 prefer 3 apply (fast)
 apply (case_tac "Finite s")
 apply (simp add: Cut_nil ForallQFilterPnil)
@@ -140,7 +140,7 @@
 
 
 lemma Cut_idemp: "Cut P (Cut P s) = (Cut P s)"
-apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P x" and x1 = "s" in
+apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P x" and x1 = "s" in
   take_lemma_less_induct [THEN mp])
 prefer 3 apply (fast)
 apply (case_tac "Finite s")
@@ -154,7 +154,7 @@
 
 
 lemma MapCut: "Map f$(Cut (P o f) s) = Cut P (Map f$s)"
-apply (rule_tac A1 = "%x. True" and Q1 = "%x.~ P (f x) " and x1 = "s" in
+apply (rule_tac A1 = "%x. True" and Q1 = "%x. \<not> P (f x) " and x1 = "s" in
   take_lemma_less_induct [THEN mp])
 prefer 3 apply (fast)
 apply (case_tac "Finite s")
diff -r 89291b5d0ede -r 8cba509ace9c src/HOL/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Wed Dec 30 21:52:00 2015 +0100
@@ -24,8 +24,8 @@
 
 Init       :: "'a predicate => 'a temporal"          ("<_>" [0] 1000)
 
-Box        :: "'a temporal => 'a temporal"   ("\<box> (_)" [80] 80)
-Diamond    :: "'a temporal => 'a temporal"   ("\<diamond> (_)" [80] 80)
+Box        :: "'a temporal => 'a temporal"   ("\<box>(_)" [80] 80)
+Diamond    :: "'a temporal => 'a temporal"   ("\<diamond>(_)" [80] 80)
 Next       :: "'a temporal => 'a temporal"
 Leadsto    :: "'a temporal => 'a temporal => 'a temporal"  (infixr "\<leadsto>" 22)
 
@@ -51,25 +51,25 @@
   "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
 
 Diamond_def:
-  "\<diamond>P == .~ (\<box>(.~ P))"
+  "\<diamond>P == \<^bold>\<not> (\<box>(\<^bold>\<not> P))"
 
 Leadsto_def:
-   "P \<leadsto> Q == (\<box>(P .--> (\<diamond>Q)))"
+   "P \<leadsto> Q == (\<box>(P \<^bold>\<longrightarrow> (\<diamond>Q)))"
 
 validT_def:
-  "validT P == ! s. s~=UU & s~=nil --> (s |= P)"
+  "validT P == ! s. s~=UU & s~=nil --> (s \<Turnstile> P)"
 
 
-lemma simple: "\<box>\<diamond>(.~ P) = (.~ \<diamond>\<box>P)"
+lemma simple: "\<box>\<diamond>(\<^bold>\<not> P) = (\<^bold>\<not> \<diamond>\<box>P)"
 apply (rule ext)
 apply (simp add: Diamond_def NOT_def Box_def)
 done
 
-lemma Boxnil: "nil |= \<box>P"
+lemma Boxnil: "nil \<Turnstile> \<box>P"
 apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)
 done
 
-lemma Diamondnil: "~(nil |= \<diamond>P)"
+lemma Diamondnil: "~(nil \<Turnstile> \<diamond>P)"
 apply (simp add: Diamond_def satisfies_def NOT_def)
 apply (cut_tac Boxnil)
 apply (simp add: satisfies_def)
@@ -89,7 +89,7 @@
 apply auto
 done
 
-lemma reflT: "s~=UU & s~=nil --> (s |= \<box>F .--> F)"
+lemma reflT: "s~=UU & s~=nil --> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> F)"
 apply (simp add: satisfies_def IMPLIES_def Box_def)
 apply (rule impI)+
 apply (erule_tac x = "s" in allE)
@@ -105,7 +105,7 @@
 apply (simp (no_asm) add: Conc_assoc)
 done
 
-lemma transT: "s |= \<box>F .--> \<box>\<box>F"
+lemma transT: "s \<Turnstile> \<box>F \<^bold>\<longrightarrow> \<box>\<box>F"
 apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def tsuffix_def)
 apply auto
 apply (drule suffix_trans)
@@ -115,7 +115,7 @@
 done
 
 
-lemma normalT: "s |= \<box>(F .--> G) .--> \<box>F .--> \<box>G"
+lemma normalT: "s \<Turnstile> \<box>(F \<^bold>\<longrightarrow> G) \<^bold>\<longrightarrow> \<box>F \<^bold>\<longrightarrow> \<box>G"
 apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def)
 done
 
@@ -136,7 +136,7 @@
 done
 
 (* Note that unlift and HD is not at all used !!! *)
-lemma STL4: "valid (P .--> Q)  ==> validT (\<box>(Init P) .--> \<box>(Init Q))"
+lemma STL4: "valid (P \<^bold>\<longrightarrow> Q)  ==> validT (\<box>(Init P) \<^bold>\<longrightarrow> \<box>(Init Q))"
 apply (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)
 done
 
@@ -156,13 +156,13 @@
 
 declare split_if [split del]
 lemma LTL1: 
-   "s~=UU & s~=nil --> (s |= \<box>F .--> (F .& (Next (\<box>F))))"
+   "s~=UU & s~=nil --> (s \<Turnstile> \<box>F \<^bold>\<longrightarrow> (F \<^bold>\<and> (Next (\<box>F))))"
 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
 apply auto
-(* \<box>F .--> F *)
+(* \<box>F \<^bold>\<longrightarrow> F *)
 apply (erule_tac x = "s" in allE)
 apply (simp add: tsuffix_def suffix_refl)
-(* \<box>F .--> Next \<box>F *)
+(* \<box>F \<^bold>\<longrightarrow> Next \<box>F *)
 apply (simp split add: split_if)
 apply auto
 apply (drule tsuffix_TL2)
@@ -173,25 +173,25 @@
 
 
 lemma LTL2a: 
-    "s |= .~ (Next F) .--> (Next (.~ F))"
+    "s \<Turnstile> \<^bold>\<not> (Next F) \<^bold>\<longrightarrow> (Next (\<^bold>\<not> F))"
 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
 apply simp
 done
 
 lemma LTL2b: 
-    "s |= (Next (.~ F)) .--> (.~ (Next F))"
+    "s \<Turnstile> (Next (\<^bold>\<not> F)) \<^bold>\<longrightarrow> (\<^bold>\<not> (Next F))"
 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
 apply simp
 done
 
 lemma LTL3: 
-"ex |= (Next (F .--> G)) .--> (Next F) .--> (Next G)"
+"ex \<Turnstile> (Next (F \<^bold>\<longrightarrow> G)) \<^bold>\<longrightarrow> (Next F) \<^bold>\<longrightarrow> (Next G)"
 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def)
 apply simp
 done
 
 
-lemma ModusPonens: "[| validT (P .--> Q); validT P |] ==> validT Q"
+lemma ModusPonens: "[| validT (P \<^bold>\<longrightarrow> Q); validT P |] ==> validT Q"
 apply (simp add: validT_def satisfies_def IMPLIES_def)
 done
 
diff -r 89291b5d0ede -r 8cba509ace9c src/HOL/HOLCF/IOA/meta_theory/TLS.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TLS.thy	Wed Dec 30 21:52:00 2015 +0100
@@ -24,7 +24,7 @@
 option_lift :: "('a => 'b) => 'b => ('a option => 'b)"
 plift       :: "('a => bool) => ('a option => bool)"
 
-temp_sat   :: "('a,'s)execution => ('a,'s)ioa_temp => bool"    (infixr "|==" 22)
+temp_sat   :: "('a,'s)execution => ('a,'s)ioa_temp => bool"    (infixr "\<TTurnstile>" 22)
 xt1        :: "'s predicate => ('a,'s)step_pred"
 xt2        :: "'a option predicate => ('a,'s)step_pred"
 
@@ -52,7 +52,7 @@
   "plift P == option_lift P False"
 
 temp_sat_def:
-  "ex |== P == ((ex2seq ex) |= P)"
+  "ex \<TTurnstile> P == ((ex2seq ex) \<Turnstile> P)"
 
 xt1_def:
   "xt1 P tr == P (fst tr)"
@@ -72,10 +72,10 @@
       )))"
 
 validTE_def:
-  "validTE P == ! ex. (ex |== P)"
+  "validTE P == ! ex. (ex \<TTurnstile> P)"
 
 validIOA_def:
-  "validIOA A P == ! ex : executions A . (ex |== P)"
+  "validIOA A P == ! ex : executions A . (ex \<TTurnstile> P)"
 
 
 axiomatization where
@@ -164,8 +164,8 @@
 
 lemma TL_TLS: 
  "[| ! s a t. (P s) & s-a--A-> t --> (Q t) |] 
-   ==> ex |== (Init (%(s,a,t). P s) .& Init (%(s,a,t). s -a--A-> t)  
-              .--> (Next (Init (%(s,a,t).Q s))))"
+   ==> ex \<TTurnstile> (Init (%(s,a,t). P s) \<^bold>\<and> Init (%(s,a,t). s -a--A-> t)  
+              \<^bold>\<longrightarrow> (Next (Init (%(s,a,t).Q s))))"
 apply (unfold Init_def Next_def temp_sat_def satisfies_def IMPLIES_def AND_def)
 
 apply clarify
diff -r 89291b5d0ede -r 8cba509ace9c src/HOL/HOLCF/IOA/meta_theory/Traces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Wed Dec 30 21:35:21 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Traces.thy	Wed Dec 30 21:52:00 2015 +0100
@@ -155,7 +155,7 @@
 
 is_wfair_def:
   "is_wfair A W ex == (inf_often (%x. fst x:W) (snd ex)
-                     | inf_often (%x.~Enabled A W (snd x)) (snd ex))"
+                     | inf_often (%x. ~ Enabled A W (snd x)) (snd ex))"
 
 sfair_ex_def:
   "sfair_ex A ex == ! W : sfair_of A.