more symbols by default, without xsymbols mode;
authorwenzelm
Thu Jul 23 22:13:42 2015 +0200 (2015-07-23)
changeset 60773d09c66a0ea10
parent 60772 a0cfa9050fa8
child 60774 6c28d8ed2488
more symbols by default, without xsymbols mode;
src/HOL/Algebra/FiniteProduct.thy
src/HOL/Algebra/Ring.thy
src/HOL/MicroJava/BV/Correct.thy
src/HOL/MicroJava/Comp/TranslCompTp.thy
src/HOL/Number_Theory/MiscAlgebra.thy
src/HOL/UNITY/Comp/Alloc.thy
src/HOL/UNITY/Comp/AllocImpl.thy
src/HOL/UNITY/Comp/Client.thy
src/HOL/UNITY/Comp/Handshake.thy
src/HOL/UNITY/Comp/Priority.thy
src/HOL/UNITY/Lift_prog.thy
src/HOL/UNITY/PPROD.thy
src/HOL/UNITY/Rename.thy
src/HOL/UNITY/SubstAx.thy
src/HOL/UNITY/Union.thy
src/HOL/UNITY/WFair.thy
     1.1 --- a/src/HOL/Algebra/FiniteProduct.thy	Thu Jul 23 16:40:47 2015 +0200
     1.2 +++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jul 23 22:13:42 2015 +0200
     1.3 @@ -296,15 +296,9 @@
     1.4  
     1.5  syntax
     1.6    "_finprod" :: "index => idt => 'a set => 'b => 'b"
     1.7 -      ("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10)
     1.8 -syntax (xsymbols)
     1.9 -  "_finprod" :: "index => idt => 'a set => 'b => 'b"
    1.10 -      ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
    1.11 -syntax (HTML output)
    1.12 -  "_finprod" :: "index => idt => 'a set => 'b => 'b"
    1.13        ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
    1.14  translations
    1.15 -  "\<Otimes>\<index>i:A. b" == "CONST finprod \<struct>\<index> (%i. b) A"
    1.16 +  "\<Otimes>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finprod \<struct>\<index> (%i. b) A"
    1.17    -- {* Beware of argument permutation! *}
    1.18  
    1.19  lemma (in comm_monoid) finprod_empty [simp]: 
    1.20 @@ -338,8 +332,7 @@
    1.21    apply (auto simp add: finprod_def)
    1.22    done
    1.23  
    1.24 -lemma finprod_one [simp]:
    1.25 -  "(\<Otimes>i:A. \<one>) = \<one>"
    1.26 +lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
    1.27  proof (induct A rule: infinite_finite_induct)
    1.28    case empty show ?case by simp
    1.29  next
     2.1 --- a/src/HOL/Algebra/Ring.thy	Thu Jul 23 16:40:47 2015 +0200
     2.2 +++ b/src/HOL/Algebra/Ring.thy	Thu Jul 23 22:13:42 2015 +0200
     2.3 @@ -36,15 +36,9 @@
     2.4  
     2.5  syntax
     2.6    "_finsum" :: "index => idt => 'a set => 'b => 'b"
     2.7 -      ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
     2.8 -syntax (xsymbols)
     2.9 -  "_finsum" :: "index => idt => 'a set => 'b => 'b"
    2.10 -      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
    2.11 -syntax (HTML output)
    2.12 -  "_finsum" :: "index => idt => 'a set => 'b => 'b"
    2.13        ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
    2.14  translations
    2.15 -  "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A"
    2.16 +  "\<Oplus>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finsum \<struct>\<index> (%i. b) A"
    2.17    -- {* Beware of argument permutation! *}
    2.18  
    2.19  
     3.1 --- a/src/HOL/MicroJava/BV/Correct.thy	Thu Jul 23 16:40:47 2015 +0200
     3.2 +++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Jul 23 22:13:42 2015 +0200
     3.3 @@ -42,7 +42,7 @@
     3.4       correct_frames G hp phi rT sig frs))))"
     3.5  
     3.6  definition correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
     3.7 -                  ("_,_ |-JVM _ [ok]"  [51,51] 50) where
     3.8 +                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50) where
     3.9  "correct_state G phi == \<lambda>(xp,hp,frs).
    3.10     case xp of
    3.11       None \<Rightarrow> (case frs of
    3.12 @@ -59,10 +59,6 @@
    3.13     | Some x \<Rightarrow> frs = []" 
    3.14  
    3.15  
    3.16 -notation (xsymbols)
    3.17 - correct_state  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
    3.18 -
    3.19 -
    3.20  lemma sup_ty_opt_OK:
    3.21    "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
    3.22    by (cases X) auto
     4.1 --- a/src/HOL/MicroJava/Comp/TranslCompTp.thy	Thu Jul 23 16:40:47 2015 +0200
     4.2 +++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy	Thu Jul 23 22:13:42 2015 +0200
     4.3 @@ -8,7 +8,9 @@
     4.4  
     4.5  (**********************************************************************)
     4.6  
     4.7 -definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd" where 
     4.8 +definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"
     4.9 +  (infixr "\<box>" 55)
    4.10 +where 
    4.11    "comb == (\<lambda> f1 f2 x0. let (xs1, x1) = f1 x0; 
    4.12                              (xs2, x2) = f2 x1 
    4.13                          in  (xs1 @ xs2, x2))"
    4.14 @@ -16,9 +18,6 @@
    4.15  definition comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a" where
    4.16    "comb_nil a == ([], a)"
    4.17  
    4.18 -notation (xsymbols)
    4.19 -  comb  (infixr "\<box>" 55)
    4.20 -
    4.21  lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
    4.22    by (simp add: comb_def comb_nil_def split_beta)
    4.23  
     5.1 --- a/src/HOL/Number_Theory/MiscAlgebra.thy	Thu Jul 23 16:40:47 2015 +0200
     5.2 +++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Thu Jul 23 22:13:42 2015 +0200
     5.3 @@ -155,12 +155,12 @@
     5.4      and a [simp]: "a : carrier G"
     5.5    shows "a (^) card(carrier G) = one G"
     5.6  proof -
     5.7 -  have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
     5.8 +  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
     5.9      by (subst (2) finprod_reindex [symmetric],
    5.10        auto simp add: Pi_def inj_on_const_mult surj_const_mult)
    5.11 -  also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
    5.12 +  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
    5.13      by (auto simp add: finprod_multf Pi_def)
    5.14 -  also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
    5.15 +  also have "(\<Otimes>x\<in>carrier G. a) = a (^) card(carrier G)"
    5.16      by (auto simp add: finprod_const)
    5.17    finally show ?thesis
    5.18  (* uses the preceeding lemma *)
     6.1 --- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 23 16:40:47 2015 +0200
     6.2 +++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 23 22:13:42 2015 +0200
     6.3 @@ -247,7 +247,7 @@
     6.4    where Network: "Network : network_spec"
     6.5  
     6.6  definition System  :: "'a systemState program"
     6.7 -  where "System = rename sysOfAlloc Alloc Join Network Join
     6.8 +  where "System = rename sysOfAlloc Alloc \<squnion> Network \<squnion>
     6.9                   (rename sysOfClient
    6.10                    (plam x: lessThan Nclients. rename client_map Client))"
    6.11  
    6.12 @@ -268,9 +268,9 @@
    6.13    defines
    6.14      System_def
    6.15        "System == rename sysOfAlloc Alloc
    6.16 -                 Join
    6.17 +                 \<squnion>
    6.18                   Network
    6.19 -                 Join
    6.20 +                 \<squnion>
    6.21                   (rename sysOfClient
    6.22                    (plam x: lessThan Nclients. rename client_map Client))"
    6.23  **)
    6.24 @@ -631,20 +631,20 @@
    6.25  
    6.26  subsection{*Components Lemmas [MUST BE AUTOMATED]*}
    6.27  
    6.28 -lemma Network_component_System: "Network Join
    6.29 +lemma Network_component_System: "Network \<squnion>
    6.30        ((rename sysOfClient
    6.31 -        (plam x: (lessThan Nclients). rename client_map Client)) Join
    6.32 +        (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
    6.33         rename sysOfAlloc Alloc)
    6.34        = System"
    6.35    by (simp add: System_def Join_ac)
    6.36  
    6.37  lemma Client_component_System: "(rename sysOfClient
    6.38 -       (plam x: (lessThan Nclients). rename client_map Client)) Join
    6.39 -      (Network Join rename sysOfAlloc Alloc)  =  System"
    6.40 +       (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
    6.41 +      (Network \<squnion> rename sysOfAlloc Alloc)  =  System"
    6.42    by (simp add: System_def Join_ac)
    6.43  
    6.44 -lemma Alloc_component_System: "rename sysOfAlloc Alloc Join
    6.45 -       ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join
    6.46 +lemma Alloc_component_System: "rename sysOfAlloc Alloc \<squnion>
    6.47 +       ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
    6.48          Network)  =  System"
    6.49    by (simp add: System_def Join_ac)
    6.50  
     7.1 --- a/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 23 16:40:47 2015 +0200
     7.2 +++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 23 22:13:42 2015 +0200
     7.3 @@ -258,21 +258,21 @@
     7.4  
     7.5  lemma Merge_Always_Out_eq_iOut:
     7.6       "[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]
     7.7 -      ==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
     7.8 +      ==> M \<squnion> G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
     7.9  apply (cut_tac Merge_spec)
    7.10  apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
    7.11  done
    7.12  
    7.13  lemma Merge_Bounded:
    7.14       "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
    7.15 -      ==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
    7.16 +      ==> M \<squnion> G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
    7.17  apply (cut_tac Merge_spec)
    7.18  apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
    7.19  done
    7.20  
    7.21  lemma Merge_Bag_Follows_lemma:
    7.22       "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
    7.23 -  ==> M Join G \<in> Always
    7.24 +  ==> M \<squnion> G \<in> Always
    7.25            {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (merge.Out s)
    7.26                                    {k. k < length (iOut s) & iOut s ! k = i})) =
    7.27                (bag_of o merge.Out) s}"
    7.28 @@ -325,8 +325,8 @@
    7.29  
    7.30  lemma Distr_Bag_Follows_lemma:
    7.31       "[| G \<in> preserves distr.Out;
    7.32 -         D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
    7.33 -  ==> D Join G \<in> Always
    7.34 +         D \<squnion> G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
    7.35 +  ==> D \<squnion> G \<in> Always
    7.36            {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)
    7.37                                    {k. k < length (iIn s) & iIn s ! k = i})) =
    7.38                bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
     8.1 --- a/src/HOL/UNITY/Comp/Client.thy	Thu Jul 23 16:40:47 2015 +0200
     8.2 +++ b/src/HOL/UNITY/Comp/Client.thy	Thu Jul 23 22:13:42 2015 +0200
     8.3 @@ -98,7 +98,7 @@
     8.4        simultaneously. *}
     8.5  lemma ask_bounded_lemma:
     8.6       "Client ok G   
     8.7 -      ==> Client Join G \<in>   
     8.8 +      ==> Client \<squnion> G \<in>   
     8.9                Always ({s. tok s \<le> NbT}  Int   
    8.10                        {s. \<forall>elt \<in> set (ask s). elt \<le> NbT})"
    8.11  apply auto
    8.12 @@ -125,13 +125,13 @@
    8.13  by (simp add: Client_def, safety, auto)
    8.14  
    8.15  lemma Join_Stable_rel_le_giv:
    8.16 -     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
    8.17 -      ==> Client Join G \<in> Stable {s. rel s \<le> giv s}"
    8.18 +     "[| Client \<squnion> G \<in> Increasing giv;  G \<in> preserves rel |]  
    8.19 +      ==> Client \<squnion> G \<in> Stable {s. rel s \<le> giv s}"
    8.20  by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto)
    8.21  
    8.22  lemma Join_Always_rel_le_giv:
    8.23 -     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
    8.24 -      ==> Client Join G \<in> Always {s. rel s \<le> giv s}"
    8.25 +     "[| Client \<squnion> G \<in> Increasing giv;  G \<in> preserves rel |]  
    8.26 +      ==> Client \<squnion> G \<in> Always {s. rel s \<le> giv s}"
    8.27  by (force intro: AlwaysI Join_Stable_rel_le_giv)
    8.28  
    8.29  lemma transient_lemma:
    8.30 @@ -146,8 +146,8 @@
    8.31  
    8.32  
    8.33  lemma induct_lemma:
    8.34 -     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
    8.35 -  ==> Client Join G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
    8.36 +     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
    8.37 +  ==> Client \<squnion> G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
    8.38                        LeadsTo {s. k < rel s & rel s \<le> giv s &  
    8.39                                    h \<le> giv s & h pfixGe ask s}"
    8.40  apply (rule single_LeadsTo_I)
    8.41 @@ -165,8 +165,8 @@
    8.42  
    8.43  
    8.44  lemma rel_progress_lemma:
    8.45 -     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
    8.46 -  ==> Client Join G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
    8.47 +     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
    8.48 +  ==> Client \<squnion> G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
    8.49                        LeadsTo {s. h \<le> rel s}"
    8.50  apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct)
    8.51  apply (auto simp add: vimage_def)
    8.52 @@ -179,8 +179,8 @@
    8.53  
    8.54  
    8.55  lemma client_progress_lemma:
    8.56 -     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
    8.57 -      ==> Client Join G \<in> {s. h \<le> giv s & h pfixGe ask s}   
    8.58 +     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
    8.59 +      ==> Client \<squnion> G \<in> {s. h \<le> giv s & h pfixGe ask s}   
    8.60                            LeadsTo {s. h \<le> rel s}"
    8.61  apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all) 
    8.62  apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L])
     9.1 --- a/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 23 16:40:47 2015 +0200
     9.2 +++ b/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 23 22:13:42 2015 +0200
     9.3 @@ -47,7 +47,7 @@
     9.4          invFG_def [THEN def_set_simp, simp]
     9.5  
     9.6  
     9.7 -lemma invFG: "(F Join G) : Always invFG"
     9.8 +lemma invFG: "(F \<squnion> G) : Always invFG"
     9.9  apply (rule AlwaysI)
    9.10  apply force
    9.11  apply (rule constrains_imp_Constrains [THEN StableI])
    9.12 @@ -56,25 +56,25 @@
    9.13  apply (unfold G_def, safety) 
    9.14  done
    9.15  
    9.16 -lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo  
    9.17 +lemma lemma2_1: "(F \<squnion> G) : ({s. NF s = k} - {s. BB s}) LeadsTo  
    9.18                                ({s. NF s = k} Int {s. BB s})"
    9.19  apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
    9.20   apply (unfold F_def, safety) 
    9.21  apply (unfold G_def, ensures_tac "cmdG") 
    9.22  done
    9.23  
    9.24 -lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo 
    9.25 +lemma lemma2_2: "(F \<squnion> G) : ({s. NF s = k} Int {s. BB s}) LeadsTo 
    9.26                                {s. k < NF s}"
    9.27  apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
    9.28   apply (unfold F_def, ensures_tac "cmdF") 
    9.29  apply (unfold G_def, safety) 
    9.30  done
    9.31  
    9.32 -lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
    9.33 +lemma progress: "(F \<squnion> G) : UNIV LeadsTo {s. m < NF s}"
    9.34  apply (rule LeadsTo_weaken_R)
    9.35  apply (rule_tac f = "NF" and l = "Suc m" and B = "{}" 
    9.36         in GreaterThan_bounded_induct)
    9.37 -(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
    9.38 +(*The inductive step is (F \<squnion> G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
    9.39  apply (auto intro!: lemma2_1 lemma2_2
    9.40              intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
    9.41  done
    10.1 --- a/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 23 16:40:47 2015 +0200
    10.2 +++ b/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 23 22:13:42 2015 +0200
    10.3 @@ -65,7 +65,7 @@
    10.4       the vertex 'UNIV' is finite by assumption *)
    10.5    
    10.6  definition system :: "state program"
    10.7 -  where "system = (JN i. Component i)"
    10.8 +  where "system = (\<Squnion>i. Component i)"
    10.9  
   10.10  
   10.11  declare highest_def [simp] lowest_def [simp]
    11.1 --- a/src/HOL/UNITY/Lift_prog.thy	Thu Jul 23 16:40:47 2015 +0200
    11.2 +++ b/src/HOL/UNITY/Lift_prog.thy	Thu Jul 23 22:13:42 2015 +0200
    11.3 @@ -178,7 +178,7 @@
    11.4  lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
    11.5  by (simp add: lift_def)
    11.6  
    11.7 -lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
    11.8 +lemma lift_Join [simp]: "lift i (F \<squnion> G) = lift i F \<squnion> lift i G"
    11.9  by (simp add: lift_def)
   11.10  
   11.11  lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
    12.1 --- a/src/HOL/UNITY/PPROD.thy	Thu Jul 23 16:40:47 2015 +0200
    12.2 +++ b/src/HOL/UNITY/PPROD.thy	Thu Jul 23 22:13:42 2015 +0200
    12.3 @@ -31,7 +31,7 @@
    12.4  lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
    12.5  by (simp add: PLam_def JN_constant)
    12.6  
    12.7 -lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
    12.8 +lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) \<squnion> (PLam I F)"
    12.9  by (unfold PLam_def, auto)
   12.10  
   12.11  lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
   12.12 @@ -184,7 +184,7 @@
   12.13      lemma reachable_lift_Join_PLam [rule_format]:
   12.14        "[| i \<notin> I;  A \<in> reachable (F i) |]
   12.15         ==> \<forall>f. f \<in> reachable (PLam I F)
   12.16 -                  --> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
   12.17 +                  --> f(i:=A) \<in> reachable (lift i (F i) \<squnion> PLam I F)"
   12.18      apply (erule reachable.induct)
   12.19      apply (ALLGOALS Clarify_tac)
   12.20      apply (erule reachable.induct)
    13.1 --- a/src/HOL/UNITY/Rename.thy	Thu Jul 23 16:40:47 2015 +0200
    13.2 +++ b/src/HOL/UNITY/Rename.thy	Thu Jul 23 22:13:42 2015 +0200
    13.3 @@ -170,7 +170,7 @@
    13.4  by (simp add: rename_def Extend.extend_SKIP)
    13.5  
    13.6  lemma rename_Join [simp]: 
    13.7 -     "bij h ==> rename h (F Join G) = rename h F Join rename h G"
    13.8 +     "bij h ==> rename h (F \<squnion> G) = rename h F \<squnion> rename h G"
    13.9  by (simp add: rename_def Extend.extend_Join)
   13.10  
   13.11  lemma rename_JN [simp]:
    14.1 --- a/src/HOL/UNITY/SubstAx.thy	Thu Jul 23 16:40:47 2015 +0200
    14.2 +++ b/src/HOL/UNITY/SubstAx.thy	Thu Jul 23 22:13:42 2015 +0200
    14.3 @@ -15,8 +15,7 @@
    14.4  definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where
    14.5      "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
    14.6  
    14.7 -notation (xsymbols)
    14.8 -  LeadsTo  (infixl " \<longmapsto>w " 60)
    14.9 +notation LeadsTo  (infixl "\<longmapsto>w" 60)
   14.10  
   14.11  
   14.12  text{*Resembles the previous definition of LeadsTo*}
    15.1 --- a/src/HOL/UNITY/Union.thy	Thu Jul 23 16:40:47 2015 +0200
    15.2 +++ b/src/HOL/UNITY/Union.thy	Thu Jul 23 22:13:42 2015 +0200
    15.3 @@ -26,34 +26,25 @@
    15.4                               \<Inter>i \<in> I. AllowedActs (F i))"
    15.5  
    15.6  definition
    15.7 -  Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
    15.8 -  where "F Join G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
    15.9 +  Join :: "['a program, 'a program] => 'a program"      (infixl "\<squnion>" 65)
   15.10 +  where "F \<squnion> G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
   15.11                               AllowedActs F \<inter> AllowedActs G)"
   15.12  
   15.13 -definition
   15.14 -  SKIP :: "'a program"
   15.15 -  where "SKIP = mk_program (UNIV, {}, UNIV)"
   15.16 +definition SKIP :: "'a program"  ("\<bottom>")
   15.17 +  where "\<bottom> = mk_program (UNIV, {}, UNIV)"
   15.18  
   15.19    (*Characterizes safety properties.  Used with specifying Allowed*)
   15.20  definition
   15.21    safety_prop :: "'a program set => bool"
   15.22    where "safety_prop X <-> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
   15.23  
   15.24 -notation (xsymbols)
   15.25 -  SKIP  ("\<bottom>") and
   15.26 -  Join  (infixl "\<squnion>" 65)
   15.27 -
   15.28  syntax
   15.29 -  "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
   15.30 -  "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
   15.31 -syntax (xsymbols)
   15.32    "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion>_./ _)" 10)
   15.33    "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion>_\<in>_./ _)" 10)
   15.34 -
   15.35  translations
   15.36 -  "JN x: A. B" == "CONST JOIN A (%x. B)"
   15.37 -  "JN x y. B" == "JN x. JN y. B"
   15.38 -  "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
   15.39 +  "\<Squnion>x \<in> A. B" == "CONST JOIN A (\<lambda>x. B)"
   15.40 +  "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B"
   15.41 +  "\<Squnion>x. B" == "CONST JOIN (CONST UNIV) (\<lambda>x. B)"
   15.42  
   15.43  
   15.44  subsection{*SKIP*}
    16.1 --- a/src/HOL/UNITY/WFair.thy	Thu Jul 23 16:40:47 2015 +0200
    16.2 +++ b/src/HOL/UNITY/WFair.thy	Thu Jul 23 22:13:42 2015 +0200
    16.3 @@ -67,8 +67,7 @@
    16.4       --{*predicate transformer: the largest set that leads to @{term B}*}
    16.5      "wlt F B == Union {A. F \<in> A leadsTo B}"
    16.6  
    16.7 -notation (xsymbols)
    16.8 -  leadsTo  (infixl "\<longmapsto>" 60)
    16.9 +notation leadsTo  (infixl "\<longmapsto>" 60)
   16.10  
   16.11  
   16.12  subsection{*transient*}