# HG changeset patch
# User wenzelm
# Date 1451507721 -3600
# Node ID 89291b5d0ede5c7e3e385787a2f110467363bd9a
# Parent  b66d2ca1f907d1337e3429c9f91a46d582aadd1c
more symbols;

diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ABP/Correctness.thy
--- a/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Correctness.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -28,11 +28,11 @@
 
 definition
   system_ioa :: "('m action, bool * 'm impl_state)ioa" where
-  "system_ioa = (env_ioa || impl_ioa)"
+  "system_ioa = (env_ioa \<parallel> impl_ioa)"
 
 definition
   system_fin_ioa :: "('m action, bool * 'm impl_state)ioa" where
-  "system_fin_ioa = (env_ioa || impl_fin_ioa)"
+  "system_fin_ioa = (env_ioa \<parallel> impl_fin_ioa)"
 
 
 axiomatization where
@@ -231,7 +231,7 @@
   srch_fin_ioa_def rsch_fin_ioa_def rsch_ioa_def sender_trans_def
   receiver_trans_def set_lemmas
 
-lemma compat_rec: "compatible receiver_ioa (srch_ioa || rsch_ioa)"
+lemma compat_rec: "compatible receiver_ioa (srch_ioa \<parallel> rsch_ioa)"
 apply (simp del: del_simps
   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
 apply simp
@@ -241,7 +241,7 @@
 done
 
 text {* 5 proofs totally the same as before *}
-lemma compat_rec_fin: "compatible receiver_ioa (srch_fin_ioa || rsch_fin_ioa)"
+lemma compat_rec_fin: "compatible receiver_ioa (srch_fin_ioa \<parallel> rsch_fin_ioa)"
 apply (simp del: del_simps
   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
 apply simp
@@ -251,7 +251,7 @@
 done
 
 lemma compat_sen: "compatible sender_ioa
-       (receiver_ioa || srch_ioa || rsch_ioa)"
+       (receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)"
 apply (simp del: del_simps
   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
 apply simp
@@ -261,7 +261,7 @@
 done
 
 lemma compat_sen_fin: "compatible sender_ioa
-       (receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"
+       (receiver_ioa \<parallel> srch_fin_ioa \<parallel> rsch_fin_ioa)"
 apply (simp del: del_simps
   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
 apply simp
@@ -271,7 +271,7 @@
 done
 
 lemma compat_env: "compatible env_ioa
-       (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+       (sender_ioa \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)"
 apply (simp del: del_simps
   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
 apply simp
@@ -281,7 +281,7 @@
 done
 
 lemma compat_env_fin: "compatible env_ioa
-       (sender_ioa || receiver_ioa || srch_fin_ioa || rsch_fin_ioa)"
+       (sender_ioa \<parallel> receiver_ioa \<parallel> srch_fin_ioa \<parallel> rsch_fin_ioa)"
 apply (simp del: del_simps
   add: compatible_def asig_of_par asig_comp_def actions_def Int_def)
 apply simp
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ABP/Impl.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -14,7 +14,7 @@
 
 definition
  impl_ioa :: "('m action, 'm impl_state)ioa" where
- "impl_ioa = (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+ "impl_ioa = (sender_ioa \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)"
 
 definition
  sen :: "'m impl_state => 'm sender_state" where
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ABP/Impl_finite.thy
--- a/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ABP/Impl_finite.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -15,7 +15,7 @@
 
 definition
   impl_fin_ioa :: "('m action, 'm impl_fin_state)ioa" where
-  "impl_fin_ioa = (sender_ioa || receiver_ioa || srch_fin_ioa ||
+  "impl_fin_ioa = (sender_ioa \<parallel> receiver_ioa \<parallel> srch_fin_ioa \<parallel>
                   rsch_fin_ioa)"
 
 definition
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/NTP/Impl.thy
--- a/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/NTP/Impl.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -15,7 +15,7 @@
 
 definition
   impl_ioa :: "('m action, 'm impl_state)ioa" where
-  impl_def: "impl_ioa == (sender_ioa || receiver_ioa || srch_ioa || rsch_ioa)"
+  impl_def: "impl_ioa == (sender_ioa \<parallel> receiver_ioa \<parallel> srch_ioa \<parallel> rsch_ioa)"
 
 definition sen :: "'m impl_state => 'm sender_state" where "sen = fst"
 definition rec :: "'m impl_state => 'm receiver_state" where "rec = fst o snd"
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ex/TrivEx.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -45,7 +45,7 @@
   "h_abs n = (n~=0)"
 
 axiomatization where
-  MC_result: "validIOA A_ioa (<>[] <%(b,a,c). b>)"
+  MC_result: "validIOA A_ioa (\<diamond>\<box><%(b,a,c). b>)"
 
 lemma h_abs_is_abstraction:
   "is_abstraction h_abs C_ioa A_ioa"
@@ -61,7 +61,7 @@
 apply (simp add: h_abs_def)
 done
 
-lemma TrivEx_abstraction: "validIOA C_ioa (<>[] <%(n,a,m). n~=0>)"
+lemma TrivEx_abstraction: "validIOA C_ioa (\<diamond>\<box><%(n,a,m). n~=0>)"
 apply (rule AbsRuleT1)
 apply (rule h_abs_is_abstraction)
 apply (rule MC_result)
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/ex/TrivEx2.thy
--- a/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/ex/TrivEx2.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -51,7 +51,7 @@
   "h_abs n = (n~=0)"
 
 axiomatization where
-  MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (<>[] <%(b,a,c). b>)"
+  MC_result: "validLIOA (A_ioa,WF A_ioa {INC}) (\<diamond>\<box><%(b,a,c). b>)"
 
 
 lemma h_abs_is_abstraction:
@@ -90,7 +90,7 @@
 
 
 lemma TrivEx2_abstraction:
-  "validLIOA C_live_ioa (<>[] <%(n,a,m). n~=0>)"
+  "validLIOA C_live_ioa (\<diamond>\<box><%(n,a,m). n~=0>)"
 apply (unfold C_live_ioa_def)
 apply (rule AbsRuleT2)
 apply (rule h_abs_is_liveabstraction)
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Abstraction.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -58,7 +58,7 @@
 (* analog to the proved thm strength_Box - proof skipped as trivial *)
 weak_Box:
 "temp_weakening P Q h
- ==> temp_weakening ([] P) ([] Q) h"
+ ==> temp_weakening (\<box>P) (\<box>Q) h"
 
 axiomatization where
 (* analog to the proved thm strength_Next - proof skipped as trivial *)
@@ -412,7 +412,7 @@
 
 lemma strength_Box:
 "[| temp_strengthening P Q h |]
-       ==> temp_strengthening ([] P) ([] Q) h"
+       ==> temp_strengthening (\<box>P) (\<box>Q) h"
 apply (unfold temp_strengthening_def state_strengthening_def temp_sat_def satisfies_def Box_def)
 apply clarify
 apply (frule ex2seq_tsuffix)
@@ -526,7 +526,7 @@
 
 lemma strength_Diamond:
 "[| temp_strengthening P Q h |]
-       ==> temp_strengthening (<> P) (<> Q) h"
+       ==> temp_strengthening (\<diamond>P) (\<diamond>Q) h"
 apply (unfold Diamond_def)
 apply (rule strength_NOT)
 apply (rule weak_Box)
@@ -536,7 +536,7 @@
 lemma strength_Leadsto:
 "[| temp_weakening P1 P2 h;
           temp_strengthening Q1 Q2 h |]
-       ==> temp_strengthening (P1 ~> Q1) (P2 ~> Q2) h"
+       ==> temp_strengthening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h"
 apply (unfold Leadsto_def)
 apply (rule strength_Box)
 apply (erule strength_IMPLIES)
@@ -548,7 +548,7 @@
 
 lemma weak_Diamond:
 "[| temp_weakening P Q h |]
-       ==> temp_weakening (<> P) (<> Q) h"
+       ==> temp_weakening (\<diamond>P) (\<diamond>Q) h"
 apply (unfold Diamond_def)
 apply (rule weak_NOT)
 apply (rule strength_Box)
@@ -558,7 +558,7 @@
 lemma weak_Leadsto:
 "[| temp_strengthening P1 P2 h;
           temp_weakening Q1 Q2 h |]
-       ==> temp_weakening (P1 ~> Q1) (P2 ~> Q2) h"
+       ==> temp_weakening (P1 \<leadsto> Q1) (P2 \<leadsto> Q2) h"
 apply (unfold Leadsto_def)
 apply (rule weak_Box)
 apply (erule weak_IMPLIES)
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/Automata.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Automata.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -57,7 +57,7 @@
   (* binary composition of action signatures and automata *)
   asig_comp    ::"['a signature, 'a signature] => 'a signature"
   compatible   ::"[('a,'s)ioa, ('a,'t)ioa] => bool"
-  par          ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "||" 10)
+  par          ::"[('a,'s)ioa, ('a,'t)ioa] => ('a,'s*'t)ioa"  (infixr "\<parallel>" 10)
 
   (* hiding and restricting *)
   hide_asig     :: "['a signature, 'a set] => 'a signature"
@@ -69,9 +69,6 @@
   rename_set    :: "'a set => ('c => 'a option) => 'c set"
   rename        :: "('a, 'b)ioa => ('c => 'a option) => ('c,'b)ioa"
 
-notation (xsymbols)
-  par  (infixr "\<parallel>" 10)
-
 
 inductive
   reachable :: "('a, 's) ioa => 's => bool"
@@ -145,7 +142,7 @@
        (internals(a1) Un internals(a2))))"
 
 par_def:
-  "(A || B) ==
+  "(A \<parallel> B) ==
       (asig_comp (asig_of A) (asig_of B),
        {pr. fst(pr):starts_of(A) & snd(pr):starts_of(B)},
        {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))
@@ -266,12 +263,12 @@
 done
 
 lemma starts_of_par: 
-"starts_of(A || B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"
+"starts_of(A \<parallel> B) = {p. fst(p):starts_of(A) & snd(p):starts_of(B)}"
   apply (simp add: par_def ioa_projections)
 done
 
 lemma trans_of_par: 
-"trans_of(A || B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))  
+"trans_of(A \<parallel> B) = {tr. let s = fst(tr); a = fst(snd(tr)); t = snd(snd(tr))  
              in (a:act A | a:act B) &  
                 (if a:act A then        
                    (fst(s),a,fst(t)):trans_of(A)  
@@ -293,38 +290,38 @@
   apply blast
   done
 
-lemma asig_of_par: "asig_of(A || B) = asig_comp (asig_of A) (asig_of B)"
+lemma asig_of_par: "asig_of(A \<parallel> B) = asig_comp (asig_of A) (asig_of B)"
   apply (simp add: par_def ioa_projections)
   done
 
 
-lemma externals_of_par: "ext (A1||A2) =     
+lemma externals_of_par: "ext (A1\<parallel>A2) =     
    (ext A1) Un (ext A2)"
 apply (simp add: externals_def asig_of_par asig_comp_def
   asig_inputs_def asig_outputs_def Un_def set_diff_eq)
 apply blast
 done
 
-lemma actions_of_par: "act (A1||A2) =     
+lemma actions_of_par: "act (A1\<parallel>A2) =     
    (act A1) Un (act A2)"
 apply (simp add: actions_def asig_of_par asig_comp_def
   asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
 apply blast
 done
 
-lemma inputs_of_par: "inp (A1||A2) = 
+lemma inputs_of_par: "inp (A1\<parallel>A2) = 
           ((inp A1) Un (inp A2)) - ((out A1) Un (out A2))"
 apply (simp add: actions_def asig_of_par asig_comp_def
   asig_inputs_def asig_outputs_def Un_def set_diff_eq)
 done
 
-lemma outputs_of_par: "out (A1||A2) = 
+lemma outputs_of_par: "out (A1\<parallel>A2) = 
           (out A1) Un (out A2)"
 apply (simp add: actions_def asig_of_par asig_comp_def
   asig_outputs_def Un_def set_diff_eq)
 done
 
-lemma internals_of_par: "int (A1||A2) = 
+lemma internals_of_par: "int (A1\<parallel>A2) = 
           (int A1) Un (int A2)"
 apply (simp add: actions_def asig_of_par asig_comp_def
   asig_inputs_def asig_outputs_def asig_internals_def Un_def set_diff_eq)
@@ -379,7 +376,7 @@
 apply blast
 done
 
-(* needed for propagation of input_enabledness from A,B to A||B *)
+(* needed for propagation of input_enabledness from A,B to A\<parallel>B *)
 lemma inpAAactB_is_inpBoroutB: 
 "[| compatible A B; a:inp A ;a:act B|] ==> a : inp B | a: out B"
 apply (unfold asig_outputs_def asig_internals_def actions_def asig_inputs_def 
@@ -396,7 +393,7 @@
      2. inputs_of_par: outputs are no longer inputs of par. This is important here *)
 lemma input_enabled_par: 
 "[| compatible A B; input_enabled A; input_enabled B|]  
-      ==> input_enabled (A||B)"
+      ==> input_enabled (A\<parallel>B)"
 apply (unfold input_enabled_def)
 apply (simp add: Let_def inputs_of_par trans_of_par)
 apply (tactic "safe_tac (Context.raw_transfer @{theory} @{theory_context Fun})")
@@ -544,49 +541,49 @@
 done
 
 
-subsection "trans_of(A||B)"
+subsection "trans_of(A\<parallel>B)"
 
 
-lemma trans_A_proj: "[|(s,a,t):trans_of (A||B); a:act A|]  
+lemma trans_A_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act A|]  
               ==> (fst s,a,fst t):trans_of A"
 apply (simp add: Let_def par_def trans_of_def)
 done
 
-lemma trans_B_proj: "[|(s,a,t):trans_of (A||B); a:act B|]  
+lemma trans_B_proj: "[|(s,a,t):trans_of (A\<parallel>B); a:act B|]  
               ==> (snd s,a,snd t):trans_of B"
 apply (simp add: Let_def par_def trans_of_def)
 done
 
-lemma trans_A_proj2: "[|(s,a,t):trans_of (A||B); a~:act A|] 
+lemma trans_A_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act A|] 
               ==> fst s = fst t"
 apply (simp add: Let_def par_def trans_of_def)
 done
 
-lemma trans_B_proj2: "[|(s,a,t):trans_of (A||B); a~:act B|] 
+lemma trans_B_proj2: "[|(s,a,t):trans_of (A\<parallel>B); a~:act B|] 
               ==> snd s = snd t"
 apply (simp add: Let_def par_def trans_of_def)
 done
 
-lemma trans_AB_proj: "(s,a,t):trans_of (A||B)  
+lemma trans_AB_proj: "(s,a,t):trans_of (A\<parallel>B)  
                ==> a :act A | a :act B"
 apply (simp add: Let_def par_def trans_of_def)
 done
 
 lemma trans_AB: "[|a:act A;a:act B; 
        (fst s,a,fst t):trans_of A;(snd s,a,snd t):trans_of B|] 
-   ==> (s,a,t):trans_of (A||B)"
+   ==> (s,a,t):trans_of (A\<parallel>B)"
 apply (simp add: Let_def par_def trans_of_def)
 done
 
 lemma trans_A_notB: "[|a:act A;a~:act B; 
        (fst s,a,fst t):trans_of A;snd s=snd t|] 
-   ==> (s,a,t):trans_of (A||B)"
+   ==> (s,a,t):trans_of (A\<parallel>B)"
 apply (simp add: Let_def par_def trans_of_def)
 done
 
 lemma trans_notA_B: "[|a~:act A;a:act B; 
        (snd s,a,snd t):trans_of B;fst s=fst t|] 
-   ==> (s,a,t):trans_of (A||B)"
+   ==> (s,a,t):trans_of (A\<parallel>B)"
 apply (simp add: Let_def par_def trans_of_def)
 done
 
@@ -595,7 +592,7 @@
 
 
 lemma trans_of_par4: 
-"((s,a,t) : trans_of(A || B || C || D)) =                                     
+"((s,a,t) : trans_of(A \<parallel> B \<parallel> C \<parallel> D)) =                                     
   ((a:actions(asig_of(A)) | a:actions(asig_of(B)) | a:actions(asig_of(C)) |   
     a:actions(asig_of(D))) &                                                  
    (if a:actions(asig_of(A)) then (fst(s),a,fst(t)):trans_of(A)               
@@ -614,8 +611,8 @@
 
 subsection "proof obligation generator for IOA requirements"
 
-(* without assumptions on A and B because is_trans_of is also incorporated in ||def *)
-lemma is_trans_of_par: "is_trans_of (A||B)"
+(* without assumptions on A and B because is_trans_of is also incorporated in \<parallel>def *)
+lemma is_trans_of_par: "is_trans_of (A\<parallel>B)"
 apply (unfold is_trans_of_def)
 apply (simp add: Let_def actions_of_par trans_of_par)
 done
@@ -635,7 +632,7 @@
 done
 
 lemma is_asig_of_par: "[| is_asig_of A; is_asig_of B; compatible A B|]   
-          ==> is_asig_of (A||B)"
+          ==> is_asig_of (A\<parallel>B)"
 apply (simp add: is_asig_of_def asig_of_par asig_comp_def compatible_def
   asig_internals_def asig_outputs_def asig_inputs_def actions_def is_asig_def)
 apply (simp add: asig_of_def)
@@ -663,7 +660,7 @@
 
 
 lemma compatible_par: 
-"[|compatible A B; compatible A C |]==> compatible A (B||C)"
+"[|compatible A B; compatible A C |]==> compatible A (B\<parallel>C)"
 apply (unfold compatible_def)
 apply (simp add: internals_of_par outputs_of_par actions_of_par)
 apply auto
@@ -671,7 +668,7 @@
 
 (*  better derive by previous one and compat_commute *)
 lemma compatible_par2: 
-"[|compatible A C; compatible B C |]==> compatible (A||B) C"
+"[|compatible A C; compatible B C |]==> compatible (A\<parallel>B) C"
 apply (unfold compatible_def)
 apply (simp add: internals_of_par outputs_of_par actions_of_par)
 apply auto
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoExecs.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -208,10 +208,10 @@
 
 
 (* --------------------------------------------------------------------- *)
-(*  Lemma_1_1a : is_ex_fr propagates from A||B to Projections A and B    *)
+(*  Lemma_1_1a : is_ex_fr propagates from A\<parallel>B to Projections A and B    *)
 (* --------------------------------------------------------------------- *)
 
-lemma lemma_1_1a: "!s. is_exec_frag (A||B) (s,xs)
+lemma lemma_1_1a: "!s. is_exec_frag (A\<parallel>B) (s,xs)
        -->  is_exec_frag A (fst s, Filter_ex2 (asig_of A)$(ProjA2$xs)) &
             is_exec_frag B (snd s, Filter_ex2 (asig_of B)$(ProjB2$xs))"
 
@@ -222,10 +222,10 @@
 
 
 (* --------------------------------------------------------------------- *)
-(*  Lemma_1_1b : is_ex_fr (A||B) implies stuttering on Projections       *)
+(*  Lemma_1_1b : is_ex_fr (A\<parallel>B) implies stuttering on Projections       *)
 (* --------------------------------------------------------------------- *)
 
-lemma lemma_1_1b: "!s. is_exec_frag (A||B) (s,xs)
+lemma lemma_1_1b: "!s. is_exec_frag (A\<parallel>B) (s,xs)
        --> stutter (asig_of A) (fst s,ProjA2$xs)  &
            stutter (asig_of B) (snd s,ProjB2$xs)"
 
@@ -237,11 +237,11 @@
 
 
 (* --------------------------------------------------------------------- *)
-(*  Lemma_1_1c : Executions of A||B have only  A- or B-actions           *)
+(*  Lemma_1_1c : Executions of A\<parallel>B have only  A- or B-actions           *)
 (* --------------------------------------------------------------------- *)
 
-lemma lemma_1_1c: "!s. (is_exec_frag (A||B) (s,xs)
-   --> Forall (%x. fst x:act (A||B)) xs)"
+lemma lemma_1_1c: "!s. (is_exec_frag (A\<parallel>B) (s,xs)
+   --> Forall (%x. fst x:act (A\<parallel>B)) xs)"
 
 apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
   @{thm is_exec_frag_def}] 1 *})
@@ -252,7 +252,7 @@
 
 
 (* ----------------------------------------------------------------------- *)
-(*  Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A||B)   *)
+(*  Lemma_1_2 : ex A, exB, stuttering and forall a:A|B implies ex (A\<parallel>B)   *)
 (* ----------------------------------------------------------------------- *)
 
 lemma lemma_1_2:
@@ -260,8 +260,8 @@
      is_exec_frag B (snd s,Filter_ex2 (asig_of B)$(ProjB2$xs)) &
      stutter (asig_of A) (fst s,(ProjA2$xs)) &
      stutter (asig_of B) (snd s,(ProjB2$xs)) &
-     Forall (%x. fst x:act (A||B)) xs
-     --> is_exec_frag (A||B) (s,xs)"
+     Forall (%x. fst x:act (A\<parallel>B)) xs
+     --> is_exec_frag (A\<parallel>B) (s,xs)"
 
 apply (tactic {* pair_induct_tac @{context} "xs" [@{thm Forall_def}, @{thm sforall_def},
   @{thm is_exec_frag_def}, @{thm stutter_def}] 1 *})
@@ -272,11 +272,11 @@
 subsection {* COMPOSITIONALITY on EXECUTION Level -- Main Theorem *}
 
 lemma compositionality_ex:
-"(ex:executions(A||B)) =
+"(ex:executions(A\<parallel>B)) =
  (Filter_ex (asig_of A) (ProjA ex) : executions A &
   Filter_ex (asig_of B) (ProjB ex) : executions B &
   stutter (asig_of A) (ProjA ex) & stutter (asig_of B) (ProjB ex) &
-  Forall (%x. fst x:act (A||B)) (snd ex))"
+  Forall (%x. fst x:act (A\<parallel>B)) (snd ex))"
 
 apply (simp (no_asm) add: executions_def ProjB_def Filter_ex_def ProjA_def starts_of_par)
 apply (tactic {* pair_tac @{context} "ex" 1 *})
@@ -293,7 +293,7 @@
 subsection {* COMPOSITIONALITY on EXECUTION Level -- for Modules *}
 
 lemma compositionality_ex_modules:
-  "Execs (A||B) = par_execs (Execs A) (Execs B)"
+  "Execs (A\<parallel>B) = par_execs (Execs A) (Execs B)"
 apply (unfold Execs_def par_execs_def)
 apply (simp add: asig_of_par)
 apply (rule set_eqI)
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoScheds.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -220,15 +220,15 @@
 
 
 (* --------------------------------------------------------------------- *)
-(*             Schedules of A||B have only  A- or B-actions              *)
+(*             Schedules of A\<parallel>B have only  A- or B-actions              *)
 (* --------------------------------------------------------------------- *)
 
 (* very similar to lemma_1_1c, but it is not checking if every action element of
    an ex is in A or B, but after projecting it onto the action schedule. Of course, this
    is the same proposition, but we cannot change this one, when then rather lemma_1_1c  *)
 
-lemma sch_actions_in_AorB: "!s. is_exec_frag (A||B) (s,xs)
-   --> Forall (%x. x:act (A||B)) (filter_act$xs)"
+lemma sch_actions_in_AorB: "!s. is_exec_frag (A\<parallel>B) (s,xs)
+   --> Forall (%x. x:act (A\<parallel>B)) (filter_act$xs)"
 
 apply (tactic {* pair_induct_tac @{context} "xs" [@{thm is_exec_frag_def}, @{thm Forall_def},
   @{thm sforall_def}] 1 *})
@@ -246,7 +246,7 @@
   --------------------------------------------------------------------------- *)
 
 lemma Mapfst_mkex_is_sch: "! exA exB s t.
-  Forall (%x. x:act (A||B)) sch  &
+  Forall (%x. x:act (A\<parallel>B)) sch  &
   Filter (%a. a:act A)$sch << filter_act$exA &
   Filter (%a. a:act B)$sch << filter_act$exB
   --> filter_act$(snd (mkex A B sch (s,exA) (t,exB))) = sch"
@@ -324,14 +324,14 @@
   --------------------------------------------------------------------------- *)
 
 lemma stutterA_mkex: "! exA exB s t.
-  Forall (%x. x:act (A||B)) sch &
+  Forall (%x. x:act (A\<parallel>B)) sch &
   Filter (%a. a:act A)$sch << filter_act$exA &
   Filter (%a. a:act B)$sch << filter_act$exB
   --> stutter (asig_of A) (s,ProjA2$(snd (mkex A B sch (s,exA) (t,exB))))"
   by (mkex_induct sch exA exB)
 
 lemma stutter_mkex_on_A: "[|
-  Forall (%x. x:act (A||B)) sch ;
+  Forall (%x. x:act (A\<parallel>B)) sch ;
   Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
   Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
   ==> stutter (asig_of A) (ProjA (mkex A B sch exA exB))"
@@ -351,7 +351,7 @@
   --------------------------------------------------------------------------- *)
 
 lemma stutterB_mkex: "! exA exB s t.
-  Forall (%x. x:act (A||B)) sch &
+  Forall (%x. x:act (A\<parallel>B)) sch &
   Filter (%a. a:act A)$sch << filter_act$exA &
   Filter (%a. a:act B)$sch << filter_act$exB
   --> stutter (asig_of B) (t,ProjB2$(snd (mkex A B sch (s,exA) (t,exB))))"
@@ -359,7 +359,7 @@
 
 
 lemma stutter_mkex_on_B: "[|
-  Forall (%x. x:act (A||B)) sch ;
+  Forall (%x. x:act (A\<parallel>B)) sch ;
   Filter (%a. a:act A)$sch << filter_act$(snd exA) ;
   Filter (%a. a:act B)$sch << filter_act$(snd exB) |]
   ==> stutter (asig_of B) (ProjB (mkex A B sch exA exB))"
@@ -380,7 +380,7 @@
   --------------------------------------------------------------------------- *)
 
 lemma filter_mkex_is_exA_tmp: "! exA exB s t.
-  Forall (%x. x:act (A||B)) sch &
+  Forall (%x. x:act (A\<parallel>B)) sch &
   Filter (%a. a:act A)$sch << filter_act$exA  &
   Filter (%a. a:act B)$sch << filter_act$exB
   --> Filter_ex2 (asig_of A)$(ProjA2$(snd (mkex A B sch (s,exA) (t,exB)))) =
@@ -416,7 +416,7 @@
 
 
 lemma filter_mkex_is_exA: "!!sch exA exB.
-  [| Forall (%a. a:act (A||B)) sch ;
+  [| Forall (%a. a:act (A\<parallel>B)) sch ;
   Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   ==> Filter_ex (asig_of A) (ProjA (mkex A B sch exA exB)) = exA"
@@ -440,7 +440,7 @@
   --------------------------------------------------------------------------- *)
 
 lemma filter_mkex_is_exB_tmp: "! exA exB s t.
-  Forall (%x. x:act (A||B)) sch &
+  Forall (%x. x:act (A\<parallel>B)) sch &
   Filter (%a. a:act A)$sch << filter_act$exA  &
   Filter (%a. a:act B)$sch << filter_act$exB
   --> Filter_ex2 (asig_of B)$(ProjB2$(snd (mkex A B sch (s,exA) (t,exB)))) =
@@ -457,7 +457,7 @@
 
 
 lemma filter_mkex_is_exB: "!!sch exA exB.
-  [| Forall (%a. a:act (A||B)) sch ;
+  [| Forall (%a. a:act (A\<parallel>B)) sch ;
   Filter (%a. a:act A)$sch = filter_act$(snd exA)  ;
   Filter (%a. a:act B)$sch = filter_act$(snd exB) |]
   ==> Filter_ex (asig_of B) (ProjB (mkex A B sch exA exB)) = exB"
@@ -478,10 +478,10 @@
 
 
 lemma mkex_actions_in_AorB: "!s t exA exB.
-  Forall (%x. x : act (A || B)) sch &
+  Forall (%x. x : act (A \<parallel> B)) sch &
   Filter (%a. a:act A)$sch << filter_act$exA  &
   Filter (%a. a:act B)$sch << filter_act$exB
-   --> Forall (%x. fst x : act (A ||B))
+   --> Forall (%x. fst x : act (A \<parallel>B))
          (snd (mkex A B sch (s,exA) (t,exB)))"
   by (mkex_induct sch exA exB)
 
@@ -492,10 +492,10 @@
 (* ------------------------------------------------------------------ *)
 
 lemma compositionality_sch:
-"(sch : schedules (A||B)) =
+"(sch : schedules (A\<parallel>B)) =
   (Filter (%a. a:act A)$sch : schedules A &
    Filter (%a. a:act B)$sch : schedules B &
-   Forall (%x. x:act (A||B)) sch)"
+   Forall (%x. x:act (A\<parallel>B)) sch)"
 apply (simp (no_asm) add: schedules_def has_schedule_def)
 apply auto
 (* ==> *)
@@ -514,7 +514,7 @@
 
 (* <== *)
 
-(* mkex is exactly the construction of exA||B out of exA, exB, and the oracle sch,
+(* mkex is exactly the construction of exA\<parallel>B out of exA, exB, and the oracle sch,
    we need here *)
 apply (rename_tac exA exB)
 apply (rule_tac x = "mkex A B sch exA exB" in bexI)
@@ -535,7 +535,7 @@
 subsection {* COMPOSITIONALITY on SCHEDULE Level -- for Modules *}
 
 lemma compositionality_sch_modules:
-  "Scheds (A||B) = par_scheds (Scheds A) (Scheds B)"
+  "Scheds (A\<parallel>B) = par_scheds (Scheds A) (Scheds B)"
 
 apply (unfold Scheds_def par_scheds_def)
 apply (simp add: asig_of_par)
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/CompoTraces.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -199,8 +199,8 @@
 
 lemma ForallAorB_mksch [rule_format]:
   "!!A B. compatible A B ==>  
-    ! schA schB. Forall (%x. x:act (A||B)) tr  
-    --> Forall (%x. x:act (A||B)) (mksch A B$tr$schA$schB)"
+    ! schA schB. Forall (%x. x:act (A\<parallel>B)) tr  
+    --> Forall (%x. x:act (A\<parallel>B)) (mksch A B$tr$schA$schB)"
 apply (tactic {* Seq_induct_tac @{context} "tr"
   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
 apply auto
@@ -253,7 +253,7 @@
     ! x y. Forall (%x. x:act A) x & Forall (%x. x:act B) y &  
            Filter (%a. a:ext A)$x = Filter (%a. a:act A)$tr &  
            Filter (%a. a:ext B)$y = Filter (%a. a:act B)$tr & 
-           Forall (%x. x:ext (A||B)) tr  
+           Forall (%x. x:ext (A\<parallel>B)) tr  
            --> Finite (mksch A B$tr$x$y)"
 
 apply (erule Seq_Finite_ind)
@@ -409,10 +409,10 @@
 "!! A B. [| compatible A B; compatible B A; 
             is_asig(asig_of A); is_asig(asig_of B) |] ==>  
   ! schA schB. Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
-  Forall (%x. x:ext (A||B)) tr &  
+  Forall (%x. x:ext (A\<parallel>B)) tr &  
   Filter (%a. a:act A)$tr << Filter (%a. a:ext A)$schA & 
   Filter (%a. a:act B)$tr << Filter (%a. a:ext B)$schB   
-  --> Filter (%a. a:ext (A||B))$(mksch A B$tr$schA$schB) = tr"
+  --> Filter (%a. a:ext (A\<parallel>B))$(mksch A B$tr$schA$schB) = tr"
 
 apply (tactic {* Seq_induct_tac @{context} "tr"
   [@{thm Forall_def}, @{thm sforall_def}, @{thm mksch_def}] 1 *})
@@ -463,7 +463,7 @@
 
 lemma FilterAmksch_is_schA: "!! A B. [| compatible A B; compatible B A;  
   is_asig(asig_of A); is_asig(asig_of B) |] ==>  
-  Forall (%x. x:ext (A||B)) tr &  
+  Forall (%x. x:ext (A\<parallel>B)) tr &  
   Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
   Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & 
   Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & 
@@ -683,7 +683,7 @@
 
 lemma FilterBmksch_is_schB: "!! A B. [| compatible A B; compatible B A;  
   is_asig(asig_of A); is_asig(asig_of B) |] ==>  
-  Forall (%x. x:ext (A||B)) tr &  
+  Forall (%x. x:ext (A\<parallel>B)) tr &  
   Forall (%x. x:act A) schA & Forall (%x. x:act B) schB &  
   Filter (%a. a:ext A)$schA = Filter (%a. a:act A)$tr & 
   Filter (%a. a:ext B)$schB = Filter (%a. a:act B)$tr & 
@@ -900,10 +900,10 @@
 lemma compositionality_tr: 
 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;  
             is_asig(asig_of A); is_asig(asig_of B)|]  
-        ==>  (tr: traces(A||B)) =  
+        ==>  (tr: traces(A\<parallel>B)) =  
              (Filter (%a. a:act A)$tr : traces A & 
               Filter (%a. a:act B)$tr : traces B & 
-              Forall (%x. x:ext(A||B)) tr)"
+              Forall (%x. x:ext(A\<parallel>B)) tr)"
 
 apply (simp (no_asm) add: traces_def has_trace_def)
 apply auto
@@ -919,7 +919,7 @@
 prefer 2
 apply (simp add: compositionality_sch)
 apply (simp add: compatibility_consequence2 externals_of_par ext1_ext2_is_not_act2)
-(* Traces of A||B have only external actions from A or B *)
+(* Traces of A\<parallel>B have only external actions from A or B *)
 apply (rule ForallPFilterP)
 
 (* <== *)
@@ -938,7 +938,7 @@
 apply assumption
 
 apply (rename_tac h1 h2 schA schB)
-(* mksch is exactly the construction of trA||B out of schA, schB, and the oracle tr,
+(* mksch is exactly the construction of trA\<parallel>B out of schA, schB, and the oracle tr,
    we need here *)
 apply (rule_tac x = "mksch A B$tr$schA$schB" in bexI)
 
@@ -961,7 +961,7 @@
 
 "!! A B. [| is_trans_of A; is_trans_of B; compatible A B; compatible B A;  
             is_asig(asig_of A); is_asig(asig_of B)|]  
- ==> Traces (A||B) = par_traces (Traces A) (Traces B)"
+ ==> Traces (A\<parallel>B) = par_traces (Traces A) (Traces B)"
 
 apply (unfold Traces_def par_traces_def)
 apply (simp add: asig_of_par)
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Compositionality.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -23,7 +23,7 @@
 done
 
 
-(* the next two theorems are only necessary, as there is no theorem ext (A||B) = ext (B||A) *)
+(* the next two theorems are only necessary, as there is no theorem ext (A\<parallel>B) = ext (B\<parallel>A) *)
 
 lemma compatibility_consequence4: "[|eA --> A ; eB & ~eA --> ~A|] ==> (eB | eA) --> A=eA"
 apply auto
@@ -46,7 +46,7 @@
              compatible A1 B1; compatible A2 B2;  
              A1 =<| A2;  
              B1 =<| B2 |]  
-         ==> (A1 || B1) =<| (A2 || B2)"
+         ==> (A1 \<parallel> B1) =<| (A2 \<parallel> B2)"
 apply (simp add: is_asig_of_def)
 apply (frule_tac A1 = "A1" in compat_commute [THEN iffD1])
 apply (frule_tac A1 = "A2" in compat_commute [THEN iffD1])
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/Deadlock.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -55,12 +55,12 @@
 *}
 
 declare split_if [split del]
-lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A||B);  
+lemma IOA_deadlock_free: "[| a : local A; Finite sch; sch : schedules (A\<parallel>B);  
              Filter (%x. x:act A)$(sch @@ a>>nil) : schedules A; compatible A B; input_enabled B |]  
-           ==> (sch @@ a>>nil) : schedules (A||B)"
+           ==> (sch @@ a>>nil) : schedules (A\<parallel>B)"
 apply (simp add: compositionality_sch locals_def)
 apply (rule conjI)
-(* a : act (A||B) *)
+(* a : act (A\<parallel>B) *)
 prefer 2
 apply (simp add: actions_of_par)
 apply (blast dest: int_is_act out_is_act)
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/LiveIOA.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -19,10 +19,10 @@
 
 definition
   WF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
-  "WF A acts = (<> [] <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
+  "WF A acts = (\<diamond>\<box><%(s,a,t) . Enabled A acts s> .--> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
 definition
   SF :: "('a,'s)ioa => 'a set => ('a,'s)ioa_temp" where
-  "SF A acts = ([] <> <%(s,a,t) . Enabled A acts s> .--> [] <> <xt2 (plift (%a. a : acts))>)"
+  "SF A acts = (\<box>\<diamond><%(s,a,t) . Enabled A acts s> .--> \<box>\<diamond><xt2 (plift (%a. a : acts))>)"
 
 definition
   liveexecutions :: "('a,'s)live_ioa => ('a,'s)execution set" where
diff -r b66d2ca1f907 -r 89291b5d0ede src/HOL/HOLCF/IOA/meta_theory/TL.thy
--- a/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Wed Dec 30 21:23:38 2015 +0100
+++ b/src/HOL/HOLCF/IOA/meta_theory/TL.thy	Wed Dec 30 21:35:21 2015 +0100
@@ -22,17 +22,12 @@
 
 unlift     ::  "'a lift => 'a"
 
-Init         ::"'a predicate => 'a temporal"          ("<_>" [0] 1000)
+Init       :: "'a predicate => 'a temporal"          ("<_>" [0] 1000)
 
-Box          ::"'a temporal => 'a temporal"   ("[] (_)" [80] 80)
-Diamond      ::"'a temporal => 'a temporal"   ("<> (_)" [80] 80)
-Next         ::"'a temporal => 'a temporal"
-Leadsto      ::"'a temporal => 'a temporal => 'a temporal"  (infixr "~>" 22)
-
-notation (xsymbols)
-  Box  ("\<box> (_)" [80] 80) and
-  Diamond  ("\<diamond> (_)" [80] 80) and
-  Leadsto  (infixr "\<leadsto>" 22)
+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)
 
 defs
 
@@ -50,37 +45,37 @@
   "tsuffix s2 s == s2 ~= nil & s2 ~= UU & suffix s2 s"
 
 Box_def:
-  "([] P) s == ! s2. tsuffix s2 s --> P s2"
+  "(\<box>P) s == ! s2. tsuffix s2 s --> P s2"
 
 Next_def:
   "(Next P) s == if (TL$s=UU | TL$s=nil) then (P s) else P (TL$s)"
 
 Diamond_def:
-  "<> P == .~ ([] (.~ P))"
+  "\<diamond>P == .~ (\<box>(.~ P))"
 
 Leadsto_def:
-   "P ~> Q == ([] (P .--> (<> Q)))"
+   "P \<leadsto> Q == (\<box>(P .--> (\<diamond>Q)))"
 
 validT_def:
   "validT P == ! s. s~=UU & s~=nil --> (s |= P)"
 
 
-lemma simple: "[] <> (.~ P) = (.~ <> [] P)"
+lemma simple: "\<box>\<diamond>(.~ P) = (.~ \<diamond>\<box>P)"
 apply (rule ext)
 apply (simp add: Diamond_def NOT_def Box_def)
 done
 
-lemma Boxnil: "nil |= [] P"
+lemma Boxnil: "nil |= \<box>P"
 apply (simp add: satisfies_def Box_def tsuffix_def suffix_def nil_is_Conc)
 done
 
-lemma Diamondnil: "~(nil |= <> P)"
+lemma Diamondnil: "~(nil |= \<diamond>P)"
 apply (simp add: Diamond_def satisfies_def NOT_def)
 apply (cut_tac Boxnil)
 apply (simp add: satisfies_def)
 done
 
-lemma Diamond_def2: "(<> F) s = (? s2. tsuffix s2 s & F s2)"
+lemma Diamond_def2: "(\<diamond>F) s = (? s2. tsuffix s2 s & F s2)"
 apply (simp add: Diamond_def NOT_def Box_def)
 done
 
@@ -94,7 +89,7 @@
 apply auto
 done
 
-lemma reflT: "s~=UU & s~=nil --> (s |= [] F .--> F)"
+lemma reflT: "s~=UU & s~=nil --> (s |= \<box>F .--> F)"
 apply (simp add: satisfies_def IMPLIES_def Box_def)
 apply (rule impI)+
 apply (erule_tac x = "s" in allE)
@@ -110,7 +105,7 @@
 apply (simp (no_asm) add: Conc_assoc)
 done
 
-lemma transT: "s |= [] F .--> [] [] F"
+lemma transT: "s |= \<box>F .--> \<box>\<box>F"
 apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def tsuffix_def)
 apply auto
 apply (drule suffix_trans)
@@ -120,14 +115,14 @@
 done
 
 
-lemma normalT: "s |= [] (F .--> G) .--> [] F .--> [] G"
+lemma normalT: "s |= \<box>(F .--> G) .--> \<box>F .--> \<box>G"
 apply (simp (no_asm) add: satisfies_def IMPLIES_def Box_def)
 done
 
 
 subsection "TLA Rules by Lamport"
 
-lemma STL1a: "validT P ==> validT ([] P)"
+lemma STL1a: "validT P ==> validT (\<box>P)"
 apply (simp add: validT_def satisfies_def Box_def tsuffix_def)
 done
 
@@ -135,13 +130,13 @@
 apply (simp add: valid_def validT_def satisfies_def Init_def)
 done
 
-lemma STL1: "valid P ==> validT ([] (Init P))"
+lemma STL1: "valid P ==> validT (\<box>(Init P))"
 apply (rule STL1a)
 apply (erule STL1b)
 done
 
 (* Note that unlift and HD is not at all used !!! *)
-lemma STL4: "valid (P .--> Q)  ==> validT ([] (Init P) .--> [] (Init Q))"
+lemma STL4: "valid (P .--> Q)  ==> validT (\<box>(Init P) .--> \<box>(Init Q))"
 apply (simp add: valid_def validT_def satisfies_def IMPLIES_def Box_def Init_def)
 done
 
@@ -161,13 +156,13 @@
 
 declare split_if [split del]
 lemma LTL1: 
-   "s~=UU & s~=nil --> (s |= [] F .--> (F .& (Next ([] F))))"
+   "s~=UU & s~=nil --> (s |= \<box>F .--> (F .& (Next (\<box>F))))"
 apply (unfold Next_def satisfies_def NOT_def IMPLIES_def AND_def Box_def)
 apply auto
-(* []F .--> F *)
+(* \<box>F .--> F *)
 apply (erule_tac x = "s" in allE)
 apply (simp add: tsuffix_def suffix_refl)
-(* []F .--> Next [] F *)
+(* \<box>F .--> Next \<box>F *)
 apply (simp split add: split_if)
 apply auto
 apply (drule tsuffix_TL2)