# HG changeset patch
# User wenzelm
# Date 1437682422 -7200
# Node ID d09c66a0ea10ebd3a6e25c9a31feee32c965011c
# Parent  a0cfa9050fa851b0e3957f91f56eb3c9224e907d
more symbols by default, without xsymbols mode;

diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -296,15 +296,9 @@
 
 syntax
   "_finprod" :: "index => idt => 'a set => 'b => 'b"
-      ("(3\<Otimes>__:_. _)" [1000, 0, 51, 10] 10)
-syntax (xsymbols)
-  "_finprod" :: "index => idt => 'a set => 'b => 'b"
-      ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
-syntax (HTML output)
-  "_finprod" :: "index => idt => 'a set => 'b => 'b"
       ("(3\<Otimes>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
-  "\<Otimes>\<index>i:A. b" == "CONST finprod \<struct>\<index> (%i. b) A"
+  "\<Otimes>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finprod \<struct>\<index> (%i. b) A"
   -- {* Beware of argument permutation! *}
 
 lemma (in comm_monoid) finprod_empty [simp]: 
@@ -338,8 +332,7 @@
   apply (auto simp add: finprod_def)
   done
 
-lemma finprod_one [simp]:
-  "(\<Otimes>i:A. \<one>) = \<one>"
+lemma finprod_one [simp]: "(\<Otimes>i\<in>A. \<one>) = \<one>"
 proof (induct A rule: infinite_finite_induct)
   case empty show ?case by simp
 next
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/Algebra/Ring.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -36,15 +36,9 @@
 
 syntax
   "_finsum" :: "index => idt => 'a set => 'b => 'b"
-      ("(3\<Oplus>__:_. _)" [1000, 0, 51, 10] 10)
-syntax (xsymbols)
-  "_finsum" :: "index => idt => 'a set => 'b => 'b"
-      ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
-syntax (HTML output)
-  "_finsum" :: "index => idt => 'a set => 'b => 'b"
       ("(3\<Oplus>__\<in>_. _)" [1000, 0, 51, 10] 10)
 translations
-  "\<Oplus>\<index>i:A. b" == "CONST finsum \<struct>\<index> (%i. b) A"
+  "\<Oplus>\<index>i\<in>A. b" \<rightleftharpoons> "CONST finsum \<struct>\<index> (%i. b) A"
   -- {* Beware of argument permutation! *}
 
 
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/MicroJava/BV/Correct.thy
--- a/src/HOL/MicroJava/BV/Correct.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/MicroJava/BV/Correct.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -42,7 +42,7 @@
      correct_frames G hp phi rT sig frs))))"
 
 definition correct_state :: "[jvm_prog,prog_type,jvm_state] \<Rightarrow> bool"
-                  ("_,_ |-JVM _ [ok]"  [51,51] 50) where
+                  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50) where
 "correct_state G phi == \<lambda>(xp,hp,frs).
    case xp of
      None \<Rightarrow> (case frs of
@@ -59,10 +59,6 @@
    | Some x \<Rightarrow> frs = []" 
 
 
-notation (xsymbols)
- correct_state  ("_,_ \<turnstile>JVM _ \<surd>"  [51,51] 50)
-
-
 lemma sup_ty_opt_OK:
   "(G \<turnstile> X <=o (OK T')) = (\<exists>T. X = OK T \<and> G \<turnstile> T \<preceq> T')"
   by (cases X) auto
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/MicroJava/Comp/TranslCompTp.thy
--- a/src/HOL/MicroJava/Comp/TranslCompTp.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/MicroJava/Comp/TranslCompTp.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -8,7 +8,9 @@
 
 (**********************************************************************)
 
-definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd" where 
+definition comb :: "['a \<Rightarrow> 'b list \<times> 'c, 'c \<Rightarrow> 'b list \<times> 'd, 'a] \<Rightarrow> 'b list \<times> 'd"
+  (infixr "\<box>" 55)
+where 
   "comb == (\<lambda> f1 f2 x0. let (xs1, x1) = f1 x0; 
                             (xs2, x2) = f2 x1 
                         in  (xs1 @ xs2, x2))"
@@ -16,9 +18,6 @@
 definition comb_nil :: "'a \<Rightarrow> 'b list \<times> 'a" where
   "comb_nil a == ([], a)"
 
-notation (xsymbols)
-  comb  (infixr "\<box>" 55)
-
 lemma comb_nil_left [simp]: "comb_nil \<box> f = f"
   by (simp add: comb_def comb_nil_def split_beta)
 
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/Number_Theory/MiscAlgebra.thy
--- a/src/HOL/Number_Theory/MiscAlgebra.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/Number_Theory/MiscAlgebra.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -155,12 +155,12 @@
     and a [simp]: "a : carrier G"
   shows "a (^) card(carrier G) = one G"
 proof -
-  have "(\<Otimes>x:carrier G. x) = (\<Otimes>x:carrier G. a \<otimes> x)"
+  have "(\<Otimes>x\<in>carrier G. x) = (\<Otimes>x\<in>carrier G. a \<otimes> x)"
     by (subst (2) finprod_reindex [symmetric],
       auto simp add: Pi_def inj_on_const_mult surj_const_mult)
-  also have "\<dots> = (\<Otimes>x:carrier G. a) \<otimes> (\<Otimes>x:carrier G. x)"
+  also have "\<dots> = (\<Otimes>x\<in>carrier G. a) \<otimes> (\<Otimes>x\<in>carrier G. x)"
     by (auto simp add: finprod_multf Pi_def)
-  also have "(\<Otimes>x:carrier G. a) = a (^) card(carrier G)"
+  also have "(\<Otimes>x\<in>carrier G. a) = a (^) card(carrier G)"
     by (auto simp add: finprod_const)
   finally show ?thesis
 (* uses the preceeding lemma *)
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/Comp/Alloc.thy
--- a/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/Alloc.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -247,7 +247,7 @@
   where Network: "Network : network_spec"
 
 definition System  :: "'a systemState program"
-  where "System = rename sysOfAlloc Alloc Join Network Join
+  where "System = rename sysOfAlloc Alloc \<squnion> Network \<squnion>
                  (rename sysOfClient
                   (plam x: lessThan Nclients. rename client_map Client))"
 
@@ -268,9 +268,9 @@
   defines
     System_def
       "System == rename sysOfAlloc Alloc
-                 Join
+                 \<squnion>
                  Network
-                 Join
+                 \<squnion>
                  (rename sysOfClient
                   (plam x: lessThan Nclients. rename client_map Client))"
 **)
@@ -631,20 +631,20 @@
 
 subsection{*Components Lemmas [MUST BE AUTOMATED]*}
 
-lemma Network_component_System: "Network Join
+lemma Network_component_System: "Network \<squnion>
       ((rename sysOfClient
-        (plam x: (lessThan Nclients). rename client_map Client)) Join
+        (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
        rename sysOfAlloc Alloc)
       = System"
   by (simp add: System_def Join_ac)
 
 lemma Client_component_System: "(rename sysOfClient
-       (plam x: (lessThan Nclients). rename client_map Client)) Join
-      (Network Join rename sysOfAlloc Alloc)  =  System"
+       (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
+      (Network \<squnion> rename sysOfAlloc Alloc)  =  System"
   by (simp add: System_def Join_ac)
 
-lemma Alloc_component_System: "rename sysOfAlloc Alloc Join
-       ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) Join
+lemma Alloc_component_System: "rename sysOfAlloc Alloc \<squnion>
+       ((rename sysOfClient (plam x: (lessThan Nclients). rename client_map Client)) \<squnion>
         Network)  =  System"
   by (simp add: System_def Join_ac)
 
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/Comp/AllocImpl.thy
--- a/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/AllocImpl.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -258,21 +258,21 @@
 
 lemma Merge_Always_Out_eq_iOut:
      "[| G \<in> preserves merge.Out; G \<in> preserves merge.iOut; M \<in> Allowed G |]
-      ==> M Join G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
+      ==> M \<squnion> G \<in> Always {s. length (merge.Out s) = length (merge.iOut s)}"
 apply (cut_tac Merge_spec)
 apply (force dest: guaranteesD simp add: merge_spec_def merge_eqOut_def)
 done
 
 lemma Merge_Bounded:
      "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
-      ==> M Join G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
+      ==> M \<squnion> G \<in> Always {s. \<forall>elt \<in> set (merge.iOut s). elt < Nclients}"
 apply (cut_tac Merge_spec)
 apply (force dest: guaranteesD simp add: merge_spec_def merge_bounded_def)
 done
 
 lemma Merge_Bag_Follows_lemma:
      "[| G \<in> preserves merge.iOut; G \<in> preserves merge.Out; M \<in> Allowed G |]
-  ==> M Join G \<in> Always
+  ==> M \<squnion> G \<in> Always
           {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (merge.Out s)
                                   {k. k < length (iOut s) & iOut s ! k = i})) =
               (bag_of o merge.Out) s}"
@@ -325,8 +325,8 @@
 
 lemma Distr_Bag_Follows_lemma:
      "[| G \<in> preserves distr.Out;
-         D Join G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
-  ==> D Join G \<in> Always
+         D \<squnion> G \<in> Always {s. \<forall>elt \<in> set (distr.iIn s). elt < Nclients} |]
+  ==> D \<squnion> G \<in> Always
           {s. (\<Sum>i \<in> lessThan Nclients. bag_of (sublist (distr.In s)
                                   {k. k < length (iIn s) & iIn s ! k = i})) =
               bag_of (sublist (distr.In s) (lessThan (length (iIn s))))}"
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/Comp/Client.thy
--- a/src/HOL/UNITY/Comp/Client.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/Client.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -98,7 +98,7 @@
       simultaneously. *}
 lemma ask_bounded_lemma:
      "Client ok G   
-      ==> Client Join G \<in>   
+      ==> Client \<squnion> G \<in>   
               Always ({s. tok s \<le> NbT}  Int   
                       {s. \<forall>elt \<in> set (ask s). elt \<le> NbT})"
 apply auto
@@ -125,13 +125,13 @@
 by (simp add: Client_def, safety, auto)
 
 lemma Join_Stable_rel_le_giv:
-     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
-      ==> Client Join G \<in> Stable {s. rel s \<le> giv s}"
+     "[| Client \<squnion> G \<in> Increasing giv;  G \<in> preserves rel |]  
+      ==> Client \<squnion> G \<in> Stable {s. rel s \<le> giv s}"
 by (rule stable_rel_le_giv [THEN Increasing_preserves_Stable], auto)
 
 lemma Join_Always_rel_le_giv:
-     "[| Client Join G \<in> Increasing giv;  G \<in> preserves rel |]  
-      ==> Client Join G \<in> Always {s. rel s \<le> giv s}"
+     "[| Client \<squnion> G \<in> Increasing giv;  G \<in> preserves rel |]  
+      ==> Client \<squnion> G \<in> Always {s. rel s \<le> giv s}"
 by (force intro: AlwaysI Join_Stable_rel_le_giv)
 
 lemma transient_lemma:
@@ -146,8 +146,8 @@
 
 
 lemma induct_lemma:
-     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
-  ==> Client Join G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
+     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
+  ==> Client \<squnion> G \<in> {s. rel s = k & k<h & h \<le> giv s & h pfixGe ask s}   
                       LeadsTo {s. k < rel s & rel s \<le> giv s &  
                                   h \<le> giv s & h pfixGe ask s}"
 apply (rule single_LeadsTo_I)
@@ -165,8 +165,8 @@
 
 
 lemma rel_progress_lemma:
-     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
-  ==> Client Join G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
+     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
+  ==> Client \<squnion> G \<in> {s. rel s < h & h \<le> giv s & h pfixGe ask s}   
                       LeadsTo {s. h \<le> rel s}"
 apply (rule_tac f = "%s. size h - size (rel s) " in LessThan_induct)
 apply (auto simp add: vimage_def)
@@ -179,8 +179,8 @@
 
 
 lemma client_progress_lemma:
-     "[| Client Join G \<in> Increasing giv;  Client ok G |]  
-      ==> Client Join G \<in> {s. h \<le> giv s & h pfixGe ask s}   
+     "[| Client \<squnion> G \<in> Increasing giv;  Client ok G |]  
+      ==> Client \<squnion> G \<in> {s. h \<le> giv s & h pfixGe ask s}   
                           LeadsTo {s. h \<le> rel s}"
 apply (rule Join_Always_rel_le_giv [THEN Always_LeadsToI], simp_all) 
 apply (rule LeadsTo_Un [THEN LeadsTo_weaken_L])
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/Comp/Handshake.thy
--- a/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/Handshake.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -47,7 +47,7 @@
         invFG_def [THEN def_set_simp, simp]
 
 
-lemma invFG: "(F Join G) : Always invFG"
+lemma invFG: "(F \<squnion> G) : Always invFG"
 apply (rule AlwaysI)
 apply force
 apply (rule constrains_imp_Constrains [THEN StableI])
@@ -56,25 +56,25 @@
 apply (unfold G_def, safety) 
 done
 
-lemma lemma2_1: "(F Join G) : ({s. NF s = k} - {s. BB s}) LeadsTo  
+lemma lemma2_1: "(F \<squnion> G) : ({s. NF s = k} - {s. BB s}) LeadsTo  
                               ({s. NF s = k} Int {s. BB s})"
 apply (rule stable_Join_ensures1[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
  apply (unfold F_def, safety) 
 apply (unfold G_def, ensures_tac "cmdG") 
 done
 
-lemma lemma2_2: "(F Join G) : ({s. NF s = k} Int {s. BB s}) LeadsTo 
+lemma lemma2_2: "(F \<squnion> G) : ({s. NF s = k} Int {s. BB s}) LeadsTo 
                               {s. k < NF s}"
 apply (rule stable_Join_ensures2[THEN leadsTo_Basis, THEN leadsTo_imp_LeadsTo])
  apply (unfold F_def, ensures_tac "cmdF") 
 apply (unfold G_def, safety) 
 done
 
-lemma progress: "(F Join G) : UNIV LeadsTo {s. m < NF s}"
+lemma progress: "(F \<squnion> G) : UNIV LeadsTo {s. m < NF s}"
 apply (rule LeadsTo_weaken_R)
 apply (rule_tac f = "NF" and l = "Suc m" and B = "{}" 
        in GreaterThan_bounded_induct)
-(*The inductive step is (F Join G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
+(*The inductive step is (F \<squnion> G) : {x. NF x = ma} LeadsTo {x. ma < NF x}*)
 apply (auto intro!: lemma2_1 lemma2_2
             intro: LeadsTo_Trans LeadsTo_Diff simp add: vimage_def)
 done
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/Comp/Priority.thy
--- a/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Comp/Priority.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -65,7 +65,7 @@
      the vertex 'UNIV' is finite by assumption *)
   
 definition system :: "state program"
-  where "system = (JN i. Component i)"
+  where "system = (\<Squnion>i. Component i)"
 
 
 declare highest_def [simp] lowest_def [simp]
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/Lift_prog.thy
--- a/src/HOL/UNITY/Lift_prog.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Lift_prog.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -178,7 +178,7 @@
 lemma lift_SKIP [simp]: "lift i SKIP = SKIP"
 by (simp add: lift_def)
 
-lemma lift_Join [simp]: "lift i (F Join G) = lift i F Join lift i G"
+lemma lift_Join [simp]: "lift i (F \<squnion> G) = lift i F \<squnion> lift i G"
 by (simp add: lift_def)
 
 lemma lift_JN [simp]: "lift j (JOIN I F) = (\<Squnion>i \<in> I. lift j (F i))"
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/PPROD.thy
--- a/src/HOL/UNITY/PPROD.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/PPROD.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -31,7 +31,7 @@
 lemma PLam_SKIP [simp]: "(plam i : I. SKIP) = SKIP"
 by (simp add: PLam_def JN_constant)
 
-lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) Join (PLam I F)"
+lemma PLam_insert: "PLam (insert i I) F = (lift i (F i)) \<squnion> (PLam I F)"
 by (unfold PLam_def, auto)
 
 lemma PLam_component_iff: "((PLam I F) \<le> H) = (\<forall>i \<in> I. lift i (F i) \<le> H)"
@@ -184,7 +184,7 @@
     lemma reachable_lift_Join_PLam [rule_format]:
       "[| i \<notin> I;  A \<in> reachable (F i) |]
        ==> \<forall>f. f \<in> reachable (PLam I F)
-                  --> f(i:=A) \<in> reachable (lift i (F i) Join PLam I F)"
+                  --> f(i:=A) \<in> reachable (lift i (F i) \<squnion> PLam I F)"
     apply (erule reachable.induct)
     apply (ALLGOALS Clarify_tac)
     apply (erule reachable.induct)
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/Rename.thy
--- a/src/HOL/UNITY/Rename.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Rename.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -170,7 +170,7 @@
 by (simp add: rename_def Extend.extend_SKIP)
 
 lemma rename_Join [simp]: 
-     "bij h ==> rename h (F Join G) = rename h F Join rename h G"
+     "bij h ==> rename h (F \<squnion> G) = rename h F \<squnion> rename h G"
 by (simp add: rename_def Extend.extend_Join)
 
 lemma rename_JN [simp]:
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/SubstAx.thy
--- a/src/HOL/UNITY/SubstAx.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/SubstAx.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -15,8 +15,7 @@
 definition LeadsTo :: "['a set, 'a set] => 'a program set" (infixl "LeadsTo" 60) where
     "A LeadsTo B == {F. F \<in> (reachable F \<inter> A) leadsTo B}"
 
-notation (xsymbols)
-  LeadsTo  (infixl " \<longmapsto>w " 60)
+notation LeadsTo  (infixl "\<longmapsto>w" 60)
 
 
 text{*Resembles the previous definition of LeadsTo*}
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/Union.thy
--- a/src/HOL/UNITY/Union.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/Union.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -26,34 +26,25 @@
                              \<Inter>i \<in> I. AllowedActs (F i))"
 
 definition
-  Join :: "['a program, 'a program] => 'a program"      (infixl "Join" 65)
-  where "F Join G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
+  Join :: "['a program, 'a program] => 'a program"      (infixl "\<squnion>" 65)
+  where "F \<squnion> G = mk_program (Init F \<inter> Init G, Acts F \<union> Acts G,
                              AllowedActs F \<inter> AllowedActs G)"
 
-definition
-  SKIP :: "'a program"
-  where "SKIP = mk_program (UNIV, {}, UNIV)"
+definition SKIP :: "'a program"  ("\<bottom>")
+  where "\<bottom> = mk_program (UNIV, {}, UNIV)"
 
   (*Characterizes safety properties.  Used with specifying Allowed*)
 definition
   safety_prop :: "'a program set => bool"
   where "safety_prop X <-> SKIP: X & (\<forall>G. Acts G \<subseteq> UNION X Acts --> G \<in> X)"
 
-notation (xsymbols)
-  SKIP  ("\<bottom>") and
-  Join  (infixl "\<squnion>" 65)
-
 syntax
-  "_JOIN1"     :: "[pttrns, 'b set] => 'b set"         ("(3JN _./ _)" 10)
-  "_JOIN"      :: "[pttrn, 'a set, 'b set] => 'b set"  ("(3JN _:_./ _)" 10)
-syntax (xsymbols)
   "_JOIN1" :: "[pttrns, 'b set] => 'b set"              ("(3\<Squnion>_./ _)" 10)
   "_JOIN"  :: "[pttrn, 'a set, 'b set] => 'b set"       ("(3\<Squnion>_\<in>_./ _)" 10)
-
 translations
-  "JN x: A. B" == "CONST JOIN A (%x. B)"
-  "JN x y. B" == "JN x. JN y. B"
-  "JN x. B" == "CONST JOIN (CONST UNIV) (%x. B)"
+  "\<Squnion>x \<in> A. B" == "CONST JOIN A (\<lambda>x. B)"
+  "\<Squnion>x y. B" == "\<Squnion>x. \<Squnion>y. B"
+  "\<Squnion>x. B" == "CONST JOIN (CONST UNIV) (\<lambda>x. B)"
 
 
 subsection{*SKIP*}
diff -r a0cfa9050fa8 -r d09c66a0ea10 src/HOL/UNITY/WFair.thy
--- a/src/HOL/UNITY/WFair.thy	Thu Jul 23 16:40:47 2015 +0200
+++ b/src/HOL/UNITY/WFair.thy	Thu Jul 23 22:13:42 2015 +0200
@@ -67,8 +67,7 @@
      --{*predicate transformer: the largest set that leads to @{term B}*}
     "wlt F B == Union {A. F \<in> A leadsTo B}"
 
-notation (xsymbols)
-  leadsTo  (infixl "\<longmapsto>" 60)
+notation leadsTo  (infixl "\<longmapsto>" 60)
 
 
 subsection{*transient*}