former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";

--- a/NEWS	Mon Dec 28 19:23:15 2015 +0100
+++ b/NEWS	Mon Dec 28 21:47:32 2015 +0100
@@ -375,6 +375,11 @@
 
 *** HOL ***
 
+* Former "xsymbols" syntax with Isabelle symbols is used by default,
+without any special print mode. Important ASCII replacement syntax
+remains available under print mode "ASCII", but less important syntax
+has been removed (see below).
+
 * Combinator to represent case distinction on products is named "case_prod",
 uniformly, discontinuing any input aliasses.  Very popular theorem aliasses
 have been retained.

--- a/src/HOL/Complete_Lattices.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Complete_Lattices.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -85,27 +85,27 @@
   with the plain constant names.
 \<close>
 
-syntax
+syntax (ASCII)
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
 
-syntax (xsymbols)
+syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
 
 translations
-  "INF x y. B"   == "INF x. INF y. B"
-  "INF x. B"     == "CONST INFIMUM CONST UNIV (%x. B)"
-  "INF x. B"     == "INF x:CONST UNIV. B"
-  "INF x:A. B"   == "CONST INFIMUM A (%x. B)"
-  "SUP x y. B"   == "SUP x. SUP y. B"
-  "SUP x. B"     == "CONST SUPREMUM CONST UNIV (%x. B)"
-  "SUP x. B"     == "SUP x:CONST UNIV. B"
-  "SUP x:A. B"   == "CONST SUPREMUM A (%x. B)"
+  "\<Sqinter>x y. B"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. B"
+  "\<Sqinter>x. B"     \<rightleftharpoons> "CONST INFIMUM CONST UNIV (\<lambda>x. B)"
+  "\<Sqinter>x. B"     \<rightleftharpoons> "\<Sqinter>x \<in> CONST UNIV. B"
+  "\<Sqinter>x\<in>A. B"   \<rightleftharpoons> "CONST INFIMUM A (\<lambda>x. B)"
+  "\<Squnion>x y. B"   \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. B"
+  "\<Squnion>x. B"     \<rightleftharpoons> "CONST SUPREMUM CONST UNIV (\<lambda>x. B)"
+  "\<Squnion>x. B"     \<rightleftharpoons> "\<Squnion>x \<in> CONST UNIV. B"
+  "\<Squnion>x\<in>A. B"   \<rightleftharpoons> "CONST SUPREMUM A (\<lambda>x. B)"
 
 print_translation \<open>
   [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
@@ -970,31 +970,31 @@
 
 subsubsection \<open>Intersections of families\<close>
 
-abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  "INTER \<equiv> INFIMUM"
+abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+  where "INTER \<equiv> INFIMUM"
 
 text \<open>
   Note: must use name @{const INTER} here instead of \<open>INT\<close>
   to allow the following syntax coexist with the plain constant name.
 \<close>
 
-syntax
-  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
-  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
-
-syntax (xsymbols)
-  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
-  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
+syntax (ASCII)
+  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3INT _./ _)" [0, 10] 10)
+  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
 
 syntax (latex output)
-  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
-  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
+  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
+  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
+
+syntax
+  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
+  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
 
 translations
-  "INT x y. B"  == "INT x. INT y. B"
-  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
-  "INT x. B"    == "INT x:CONST UNIV. B"
-  "INT x:A. B"  == "CONST INTER A (%x. B)"
+  "\<Inter>x y. B"  \<rightleftharpoons> "\<Inter>x. \<Inter>y. B"
+  "\<Inter>x. B"    \<rightleftharpoons> "CONST INTER CONST UNIV (\<lambda>x. B)"
+  "\<Inter>x. B"    \<rightleftharpoons> "\<Inter>x \<in> CONST UNIV. B"
+  "\<Inter>x\<in>A. B"  \<rightleftharpoons> "CONST INTER A (\<lambda>x. B)"
 
 print_translation \<open>
   [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
@@ -1143,39 +1143,36 @@
 
 subsubsection \<open>Unions of families\<close>
 
-abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
-  "UNION \<equiv> SUPREMUM"
+abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
+  where "UNION \<equiv> SUPREMUM"
 
 text \<open>
   Note: must use name @{const UNION} here instead of \<open>UN\<close>
   to allow the following syntax coexist with the plain constant name.
 \<close>
 
-syntax
+syntax (ASCII)
   "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
 
-syntax (xsymbols)
-  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
-  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
-
 syntax (latex output)
   "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
 
+syntax
+  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
+  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
+
 translations
-  "UN x y. B"   == "UN x. UN y. B"
-  "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"
-  "UN x. B"     == "UN x:CONST UNIV. B"
-  "UN x:A. B"   == "CONST UNION A (%x. B)"
+  "\<Union>x y. B"   \<rightleftharpoons> "\<Union>x. \<Union>y. B"
+  "\<Union>x. B"     \<rightleftharpoons> "CONST UNION CONST UNIV (\<lambda>x. B)"
+  "\<Union>x. B"     \<rightleftharpoons> "\<Union>x \<in> CONST UNIV. B"
+  "\<Union>x\<in>A. B"   \<rightleftharpoons> "CONST UNION A (\<lambda>x. B)"
 
 text \<open>
-  Note the difference between ordinary xsymbol syntax of indexed
+  Note the difference between ordinary syntax of indexed
   unions and intersections (e.g.\ \<open>\<Union>a\<^sub>1\<in>A\<^sub>1. B\<close>)
-  and their \LaTeX\ rendition: @{term"\<Union>a\<^sub>1\<in>A\<^sub>1. B"}. The
-  former does not make the index expression a subscript of the
-  union/intersection symbol because this leads to problems with nested
-  subscripts in Proof General.
+  and their \LaTeX\ rendition: @{term"\<Union>a\<^sub>1\<in>A\<^sub>1. B"}.
 \<close>
 
 print_translation \<open>

--- a/src/HOL/Filter.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Filter.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -693,19 +693,20 @@
 lemma eventually_sequentially_seg: "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
   using eventually_sequentially_Suc[of "\<lambda>n. P (n + k)" for k] by (induction k) auto
 
-subsection \<open> The cofinite filter \<close>
+
+subsection \<open>The cofinite filter\<close>
 
 definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
 
-abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
-  "Inf_many P \<equiv> frequently P cofinite"
+abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>\<^sub>\<infinity>" 10)
+  where "Inf_many P \<equiv> frequently P cofinite"
 
-abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
-  "Alm_all P \<equiv> eventually P cofinite"
+abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>\<^sub>\<infinity>" 10)
+  where "Alm_all P \<equiv> eventually P cofinite"
 
-notation (xsymbols)
-  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
-  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
+notation (ASCII)
+  Inf_many  (binder "INFM " 10) and
+  Alm_all  (binder "MOST " 10)
 
 lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
   unfolding cofinite_def

--- a/src/HOL/Fun.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Fun.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -42,11 +42,11 @@
 
 subsection \<open>The Composition Operator \<open>f \<circ> g\<close>\<close>
 
-definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
-  "f o g = (\<lambda>x. f (g x))"
+definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl "\<circ>" 55)
+  where "f \<circ> g = (\<lambda>x. f (g x))"
 
-notation (xsymbols)
-  comp  (infixl "\<circ>" 55)
+notation (ASCII)
+  comp  (infixl "o" 55)
 
 lemma comp_apply [simp]: "(f o g) x = f (g x)"
   by (simp add: comp_def)

--- a/src/HOL/Groups_Big.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Groups_Big.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -471,35 +471,28 @@
 defines
   setsum = setsum.F ..
 
-abbreviation
-  Setsum ("\<Sum>_" [1000] 999) where
-  "\<Sum>A \<equiv> setsum (%x. x) A"
+abbreviation Setsum ("\<Sum>_" [1000] 999)
+  where "\<Sum>A \<equiv> setsum (\<lambda>x. x) A"
 
 end
 
-text\<open>Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
-written \<open>\<Sum>x\<in>A. e\<close>.\<close>
+text \<open>Now: lot's of fancy syntax. First, @{term "setsum (\<lambda>x. e) A"} is written \<open>\<Sum>x\<in>A. e\<close>.\<close>
 
+syntax (ASCII)
+  "_setsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(3SUM _:_./ _)" [0, 51, 10] 10)
 syntax
-  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_./ _)" [0, 51, 10] 10)
-syntax (xsymbols)
-  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
-
+  "_setsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
 translations \<comment> \<open>Beware of argument permutation!\<close>
-  "SUM i:A. b" == "CONST setsum (%i. b) A"
-  "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
+  "\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST setsum (\<lambda>i. b) A"
 
-text\<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
- \<open>\<Sum>x|P. e\<close>.\<close>
+text \<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>
 
+syntax (ASCII)
+  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SUM _ |/ _./ _)" [0, 0, 10] 10)
 syntax
-  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
-syntax (xsymbols)
-  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
-
+  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Sum>_ | (_)./ _)" [0, 0, 10] 10)
 translations
-  "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
-  "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
+  "\<Sum>x|P. t" => "CONST setsum (\<lambda>x. t) {x. P}"
 
 print_translation \<open>
 let
@@ -1059,26 +1052,21 @@
 
 end
 
-syntax
+syntax (ASCII)
   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
-syntax (xsymbols)
+syntax
   "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
-
 translations \<comment> \<open>Beware of argument permutation!\<close>
-  "PROD i:A. b" == "CONST setprod (%i. b) A" 
-  "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
+  "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A" 
 
-text\<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
- \<open>\<Prod>x|P. e\<close>.\<close>
+text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
 
+syntax (ASCII)
+  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
 syntax
-  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
-syntax (xsymbols)
-  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
-
+  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
 translations
-  "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
-  "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
+  "\<Prod>x|P. t" => "CONST setprod (\<lambda>x. t) {x. P}"
 
 context comm_monoid_mult
 begin

--- a/src/HOL/Groups_List.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Groups_List.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -93,15 +93,12 @@
 end
 
 text \<open>Some syntactic sugar for summing a function over a list:\<close>
-
+syntax (ASCII)
+  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
 syntax
-  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
-syntax (xsymbols)
   "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
-
 translations \<comment> \<open>Beware of argument permutation!\<close>
-  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
-  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
+  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (\<lambda>x. b) xs)"
 
 text \<open>TODO duplicates\<close>
 lemmas listsum_simps = listsum.Nil listsum.Cons
@@ -352,13 +349,11 @@
 
 text \<open>Some syntactic sugar:\<close>
 
-syntax
+syntax (ASCII)
   "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
-syntax (xsymbols)
+syntax
   "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
-
 translations \<comment> \<open>Beware of argument permutation!\<close>
-  "PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
-  "\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)"
+  "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST listprod (CONST map (\<lambda>x. b) xs)"
 
 end

--- a/src/HOL/HOL.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/HOL.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -73,48 +73,45 @@
   Trueprop      :: "bool \<Rightarrow> prop"                   ("(_)" 5)
 
 axiomatization
-  implies       :: "[bool, bool] \<Rightarrow> bool"           (infixr "-->" 25)  and
+  implies       :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<longrightarrow>" 25)  and
   eq            :: "['a, 'a] \<Rightarrow> bool"               (infixl "=" 50)  and
   The           :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
 
 consts
   True          :: bool
   False         :: bool
-  Not           :: "bool \<Rightarrow> bool"                   ("~ _" [40] 40)
+  Not           :: "bool \<Rightarrow> bool"                   ("\<not> _" [40] 40)
 
-  conj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "&" 35)
-  disj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "|" 30)
+  conj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<and>" 35)
+  disj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<or>" 30)
 
-  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "ALL " 10)
-  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "EX " 10)
-  Ex1           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "EX! " 10)
+  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<forall>" 10)
+  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>" 10)
+  Ex1           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>!" 10)
 
 
 subsubsection \<open>Additional concrete syntax\<close>
 
-notation (output)
-  eq  (infix "=" 50)
-
-abbreviation
-  not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "~=" 50) where
-  "x ~= y \<equiv> ~ (x = y)"
+abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<noteq>" 50)
+  where "x \<noteq> y \<equiv> \<not> (x = y)"
 
 notation (output)
+  eq  (infix "=" 50) and
+  not_equal  (infix "\<noteq>" 50)
+
+notation (ASCII output)
   not_equal  (infix "~=" 50)
 
-notation (xsymbols)
-  Not  ("\<not> _" [40] 40) and
-  conj  (infixr "\<and>" 35) and
-  disj  (infixr "\<or>" 30) and
-  implies  (infixr "\<longrightarrow>" 25) and
-  not_equal  (infixl "\<noteq>" 50)
-
-notation (xsymbols output)
-  not_equal  (infix "\<noteq>" 50)
+notation (ASCII)
+  Not  ("~ _" [40] 40) and
+  conj  (infixr "&" 35) and
+  disj  (infixr "|" 30) and
+  implies  (infixr "-->" 25) and
+  not_equal  (infixl "~=" 50)
 
 abbreviation (iff)
-  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25) where
-  "A \<longleftrightarrow> B \<equiv> A = B"
+  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25)
+  where "A \<longleftrightarrow> B \<equiv> A = B"
 
 syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
 translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
@@ -134,16 +131,16 @@
 nonterminal case_syn and cases_syn
 syntax
   "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  ("(case _ of/ _)" 10)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ =>/ _)" 10)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
   "" :: "case_syn \<Rightarrow> cases_syn"  ("_")
   "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  ("_/ | _")
-syntax (xsymbols)
-  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
+syntax (ASCII)
+  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ =>/ _)" 10)
 
-notation (xsymbols)
-  All  (binder "\<forall>" 10) and
-  Ex  (binder "\<exists>" 10) and
-  Ex1  (binder "\<exists>!" 10)
+notation (ASCII)
+  All  (binder "ALL " 10) and
+  Ex  (binder "EX " 10) and
+  Ex1  (binder "EX! " 10)
 
 notation (HOL)
   All  (binder "! " 10) and

--- a/src/HOL/Inductive.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Inductive.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -370,13 +370,11 @@
 ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
 ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
 
-text\<open>Lambda-abstractions with pattern matching:\<close>
-
+text \<open>Lambda-abstractions with pattern matching:\<close>
+syntax (ASCII)
+  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(%_)" 10)
 syntax
-  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(%_)" 10)
-syntax (xsymbols)
-  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
-
+  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(\<lambda>_)" 10)
 parse_translation \<open>
   let
     fun fun_tr ctxt [cs] =

--- a/src/HOL/Library/FinFun.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/FinFun.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -907,10 +907,11 @@
 
 subsection \<open>Function composition\<close>
 
-definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "o$" 55)
-where [code del]: "g o$ f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
+definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b"  (infixr "\<circ>$" 55)
+where [code del]: "g \<circ>$ f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
 
-notation (xsymbols) finfun_comp (infixr "\<circ>$" 55)
+notation (ASCII)
+  finfun_comp (infixr "o$" 55)
 
 interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
 by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
@@ -968,10 +969,11 @@
   thus ?thesis by(auto simp add: fun_eq_iff)
 qed
 
-definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "$o" 55)
-where [code del]: "g $o f = Abs_finfun (op $ g \<circ> f)"
+definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c"  (infixr "$\<circ>" 55)
+where [code del]: "g $\<circ> f = Abs_finfun (op $ g \<circ> f)"
 
-notation (xsymbol) finfun_comp2 (infixr "$\<circ>" 55)
+notation (ASCII)
+  finfun_comp2  (infixr "$o" 55)
 
 lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K$ c) f = (K$ c)"
   including finfun
@@ -1534,12 +1536,12 @@
   finfun_const ("K$/ _" [0] 1) and
   finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
   finfun_apply (infixl "$" 999) and
-  finfun_comp (infixr "o$" 55) and
-  finfun_comp2 (infixr "$o" 55) and
+  finfun_comp (infixr "\<circ>$" 55) and
+  finfun_comp2 (infixr "$\<circ>" 55) and
   finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
 
-no_notation (xsymbols) 
-  finfun_comp (infixr "\<circ>$" 55) and
-  finfun_comp2 (infixr "$\<circ>" 55)
+no_notation (ASCII) 
+  finfun_comp (infixr "o$" 55) and
+  finfun_comp2 (infixr "$o" 55)
 
 end

--- a/src/HOL/Library/FinFun_Syntax.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/FinFun_Syntax.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -13,12 +13,12 @@
   finfun_const ("K$/ _" [0] 1) and
   finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
   finfun_apply (infixl "$" 999) and
-  finfun_comp (infixr "o$" 55) and
-  finfun_comp2 (infixr "$o" 55) and
+  finfun_comp (infixr "\<circ>$" 55) and
+  finfun_comp2 (infixr "$\<circ>" 55) and
   finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
 
-notation (xsymbols) 
-  finfun_comp (infixr "\<circ>$" 55) and
-  finfun_comp2 (infixr "$\<circ>" 55)
+notation (ASCII)
+  finfun_comp (infixr "o$" 55) and
+  finfun_comp2 (infixr "$o" 55)
 
 end
\ No newline at end of file

--- a/src/HOL/Library/FuncSet.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/FuncSet.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -20,10 +20,10 @@
 abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "\<rightarrow>" 60)
   where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
 
-syntax
+syntax (ASCII)
   "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
   "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
-syntax (xsymbols)
+syntax
   "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
   "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
 translations
@@ -347,11 +347,12 @@
 
 abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
 
-syntax
+syntax (ASCII)
   "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
-syntax (xsymbols)
+syntax
   "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
-translations "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
+translations
+  "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
 
 abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>E" 60)
   where "A \<rightarrow>\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"

--- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -233,12 +233,12 @@
 
 end
 
-syntax
+syntax (ASCII)
   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
-syntax (xsymbols)
+syntax
   "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
 translations
-  "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
+  "\<Sum>a. b" \<rightleftharpoons> "CONST Sum_any (\<lambda>a. b)"
 
 lemma Sum_any_left_distrib:
   fixes r :: "'a :: semiring_0"
@@ -302,10 +302,10 @@
 
 end
 
+syntax (ASCII)
+  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _. _)" [0, 10] 10)
 syntax
-  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
-syntax (xsymbols)
-  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
+  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_. _)" [0, 10] 10)
 translations
   "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
 

--- a/src/HOL/Library/Lattice_Syntax.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/Lattice_Syntax.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -14,7 +14,7 @@
   Inf  ("\<Sqinter>_" [900] 900) and
   Sup  ("\<Squnion>_" [900] 900)
 
-syntax (xsymbols)
+syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)

--- a/src/HOL/Library/Monad_Syntax.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -15,42 +15,42 @@
 \<close>
 
 consts
-  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr ">>=" 54)
+  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<guillemotright>=" 54)
 
-notation (xsymbols)
-  bind (infixr "\<guillemotright>=" 54)
+notation (ASCII)
+  bind (infixr ">>=" 54)
 
 notation (latex output)
   bind (infixr "\<bind>" 54)
 
+
 abbreviation (do_notation)
   bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
-where
-  "bind_do \<equiv> bind"
+  where "bind_do \<equiv> bind"
 
 notation (output)
-  bind_do (infixr ">>=" 54)
+  bind_do (infixr "\<guillemotright>=" 54)
 
-notation (xsymbols output)
-  bind_do (infixr "\<guillemotright>=" 54)
+notation (ASCII output)
+  bind_do (infixr ">>=" 54)
 
 notation (latex output)
   bind_do (infixr "\<bind>" 54)
 
+
 nonterminal do_binds and do_bind
-
 syntax
   "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
-  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
+  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
   "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
   "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
   "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
   "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
 
-syntax (xsymbols)
-  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
-  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
+syntax (ASCII)
+  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
 
 syntax (latex output)
   "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)

--- a/src/HOL/Library/Multiset.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/Multiset.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -25,11 +25,11 @@
 
 setup_lifting type_definition_multiset
 
-abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  ("(_/ :# _)" [50, 51] 50) where
-  "a :# M == 0 < count M a"
-
-notation (xsymbols)
-  Melem (infix "\<in>#" 50)
+abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<in>#" 50)
+  where "a \<in># M \<equiv> 0 < count M a"
+
+notation (ASCII)
+  Melem  ("(_/ :# _)" [50, 51] 50)  (* FIXME !? *)
 
 lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
   by (simp only: count_inject [symmetric] fun_eq_iff)
@@ -265,16 +265,18 @@
 
 subsubsection \<open>Pointwise ordering induced by count\<close>
 
-definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
-"subseteq_mset A B = (\<forall>a. count A a \<le> count B a)"
-
-definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
-"subset_mset A B = (A <=# B \<and> A \<noteq> B)"
-
-notation subseteq_mset (infix "\<le>#" 50)
-notation (xsymbols) subseteq_mset (infix "\<subseteq>#" 50)
-
-notation (xsymbols) subset_mset (infix "\<subset>#" 50)
+definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
+  where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)"
+
+definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
+  where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
+
+notation (input)
+  subseteq_mset  (infix "\<le>#" 50)
+
+notation (ASCII)
+  subseteq_mset  (infix "<=#" 50) and
+  subset_mset  (infix "<#" 50)
 
 interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
   by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
@@ -504,9 +506,9 @@
   show ?thesis unfolding B by auto
 qed
 
-syntax
+syntax (ASCII)
   "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
-syntax (xsymbol)
+syntax
   "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
 translations
   "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
@@ -855,27 +857,17 @@
 lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
   by (cases M) auto
 
+syntax (ASCII)
+  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
 syntax
-  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
-      ("({#_/. _ :# _#})")
-translations
-  "{#e. x:#M#}" == "CONST image_mset (\<lambda>x. e) M"
-
-syntax (xsymbols)
-  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
-      ("({#_/. _ \<in># _#})")
+  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ \<in># _#})")
 translations
-  "{#e. x \<in># M#}" == "CONST image_mset (\<lambda>x. e) M"
-
+  "{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
+
+syntax (ASCII)
+  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ :# _./ _#})")
 syntax
-  "_comprehension3_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
-      ("({#_/ | _ :# _./ _#})")
-translations
-  "{#e | x:#M. P#}" \<rightharpoonup> "{#e. x :# {# x:#M. P#}#}"
-
-syntax
-  "_comprehension4_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
-      ("({#_/ | _ \<in># _./ _#})")
+  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ \<in># _./ _#})")
 translations
   "{#e | x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}"
 
@@ -1235,10 +1227,8 @@
 qed
 
 
-abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
-  "Union_mset MM \<equiv> msetsum MM"
-
-notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
+abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
+  where "\<Union># MM \<equiv> msetsum MM"
 
 lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
   by (induct MM) auto
@@ -1246,14 +1236,12 @@
 lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
   by (induct MM) auto
 
+syntax (ASCII)
+  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
 syntax
-  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
-      ("(3SUM _:#_. _)" [0, 51, 10] 10)
-syntax (xsymbols)
-  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
-      ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
+  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
 translations
-  "SUM i :# A. b" == "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
+  "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
 
 context comm_monoid_mult
 begin
@@ -1287,14 +1275,12 @@
 
 end
 
+syntax (ASCII)
+  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _:#_. _)" [0, 51, 10] 10)
 syntax
-  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
-      ("(3PROD _:#_. _)" [0, 51, 10] 10)
-syntax (xsymbols)
-  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
-      ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
+  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
 translations
-  "PROD i :# A. b" == "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
+  "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
 
 lemma (in comm_semiring_1) dvd_msetprod:
   assumes "x \<in># A"
@@ -1718,14 +1704,15 @@
 
 subsubsection \<open>Partial-order properties\<close>
 
-definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<#" 50) where
-  "M' #<# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
-
-definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<=#" 50) where
-  "M' #<=# M \<longleftrightarrow> M' #<# M \<or> M' = M"
-
-notation (xsymbols) less_multiset (infix "#\<subset>#" 50)
-notation (xsymbols) le_multiset (infix "#\<subseteq>#" 50)
+definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "#\<subset>#" 50)
+  where "M' #\<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
+
+definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "#\<subseteq>#" 50)
+  where "M' #\<subseteq># M \<longleftrightarrow> M' #\<subset># M \<or> M' = M"
+
+notation (ASCII)
+  less_multiset (infix "#<#" 50) and
+  le_multiset (infix "#<=#" 50)
 
 interpretation multiset_order: order le_multiset less_multiset
 proof -

--- a/src/HOL/Library/Option_ord.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/Option_ord.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -16,7 +16,7 @@
   Inf  ("\<Sqinter>_" [900] 900) and
   Sup  ("\<Squnion>_" [900] 900)
 
-syntax (xsymbols)
+syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
@@ -348,7 +348,7 @@
   Inf  ("\<Sqinter>_" [900] 900) and
   Sup  ("\<Squnion>_" [900] 900)
 
-no_syntax (xsymbols)
+no_syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)

--- a/src/HOL/Library/OptionalSugar.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/OptionalSugar.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -63,7 +63,7 @@
 
 (* sorts as intersections *)
 
-syntax (xsymbols output)
+syntax (output)
   "_topsort" :: "sort"  ("\<top>" 1000)
   "_sort" :: "classes => sort"  ("'(_')" 1000)
   "_classes" :: "id => classes => classes"  ("_ \<inter> _" 1000)

--- a/src/HOL/Library/State_Monad.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Library/State_Monad.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -118,14 +118,14 @@
 
 syntax
   "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
-  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
+  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
   "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
   "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
   "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
   "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
 
-syntax (xsymbols)
-  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
+syntax (ASCII)
+  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
 
 translations
   "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"

--- a/src/HOL/List.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/List.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -77,13 +77,13 @@
 "filter P [] = []" |
 "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
 
+text \<open>Special syntax for filter:\<close>
+syntax (ASCII)
+  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_<-_./ _])")
 syntax
-  \<comment> \<open>Special syntax for filter\<close>
-  "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
-syntax (xsymbols)
-  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
+  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_\<leftarrow>_ ./ _])")
 translations
-  "[x<-xs . P]"== "CONST filter (%x. P) xs"
+  "[x<-xs . P]" \<rightleftharpoons> "CONST filter (\<lambda>x. P) xs"
 
 primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
 fold_Nil:  "fold f [] = id" |
@@ -395,13 +395,16 @@
 
 syntax
   "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
-  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
+  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
   "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
   (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
   "_lc_end" :: "lc_quals" ("]")
   "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals"  (", __")
   "_lc_abs" :: "'a => 'b list => 'b list"
 
+syntax (ASCII)
+  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
+
 (* These are easier than ML code but cannot express the optimized
    translation of [e. p<-xs]
 translations
@@ -415,9 +418,6 @@
    => "_Let b (_listcompr e Q Qs)"
 *)
 
-syntax (xsymbols)
-  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
-
 parse_translation \<open>
   let
     val NilC = Syntax.const @{const_syntax Nil};

--- a/src/HOL/Main.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Main.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -35,7 +35,7 @@
 
 hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
 
-no_syntax (xsymbols)
+no_syntax
   "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)

--- a/src/HOL/Map.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Map.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -47,16 +47,16 @@
 nonterminal maplets and maplet
 
 syntax
-  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /|->/ _")
-  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[|->]/ _")
+  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /\<mapsto>/ _")
+  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[\<mapsto>]/ _")
   ""         :: "maplet \<Rightarrow> maplets"             ("_")
   "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _")
-  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [900,0]900)
+  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [900, 0] 900)
   "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"            ("(1[_])")
 
-syntax (xsymbols)
-  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /\<mapsto>/ _")
-  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[\<mapsto>]/ _")
+syntax (ASCII)
+  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /|->/ _")
+  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[|->]/ _")
 
 translations
   "_MapUpd m (_Maplets xy ms)"  \<rightleftharpoons> "_MapUpd (_MapUpd m xy) ms"
@@ -65,15 +65,13 @@
   "_Map (_Maplets ms1 ms2)"     \<leftharpoondown> "_MapUpd (_Map ms1) ms2"
   "_Maplets ms1 (_Maplets ms2 ms3)" \<leftharpoondown> "_Maplets (_Maplets ms1 ms2) ms3"
 
-primrec
-  map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
-    "map_of [] = empty"
-  | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
+primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b"
+where
+  "map_of [] = empty"
+| "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
 
-definition
-  map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b" where
-  "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
-
+definition map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b"
+  where "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
 translations
   "_MapUpd m (_maplets x y)" \<rightleftharpoons> "CONST map_upds m x y"
 

--- a/src/HOL/Orderings.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Orderings.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -93,25 +93,25 @@
 begin
 
 notation
-  less_eq  ("op <=") and
-  less_eq  ("(_/ <= _)" [51, 51] 50) and
+  less_eq  ("op \<le>") and
+  less_eq  ("(_/ \<le> _)"  [51, 51] 50) and
   less  ("op <") and
   less  ("(_/ < _)"  [51, 51] 50)
 
-notation (xsymbols)
-  less_eq  ("op \<le>") and
-  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
+abbreviation (input)
+  greater_eq  (infix "\<ge>" 50)
+  where "x \<ge> y \<equiv> y \<le> x"
 
 abbreviation (input)
-  greater_eq  (infix ">=" 50) where
-  "x >= y \<equiv> y <= x"
+  greater  (infix ">" 50)
+  where "x > y \<equiv> y < x"
+
+notation (ASCII)
+  less_eq  ("op <=") and
+  less_eq  ("(_/ <= _)" [51, 51] 50)
 
 notation (input)
-  greater_eq  (infix "\<ge>" 50)
-
-abbreviation (input)
-  greater  (infix ">" 50) where
-  "x > y \<equiv> y < x"
+  greater_eq  (infix ">=" 50)
 
 end
 
@@ -652,7 +652,7 @@
 
 subsection \<open>Bounded quantifiers\<close>
 
-syntax
+syntax (ASCII)
   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3EX _<_./ _)"  [0, 0, 10] 10)
   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _<=_./ _)" [0, 0, 10] 10)
@@ -663,7 +663,7 @@
   "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _>=_./ _)" [0, 0, 10] 10)
   "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3EX _>=_./ _)" [0, 0, 10] 10)
 
-syntax (xsymbols)
+syntax
   "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)

--- a/src/HOL/Power.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Power.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -27,21 +27,17 @@
 class power = one + times
 begin
 
-primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where
-    power_0: "a ^ 0 = 1"
-  | power_Suc: "a ^ Suc n = a * a ^ n"
+primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixr "^" 80)
+where
+  power_0: "a ^ 0 = 1"
+| power_Suc: "a ^ Suc n = a * a ^ n"
 
 notation (latex output)
   power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
 
 text \<open>Special syntax for squares.\<close>
-
-abbreviation (xsymbols)
-  power2 :: "'a \<Rightarrow> 'a"  ("(_\<^sup>2)" [1000] 999) where
-  "x\<^sup>2 \<equiv> x ^ 2"
-
-notation (latex output)
-  power2  ("(_\<^sup>2)" [1000] 999)
+abbreviation power2 :: "'a \<Rightarrow> 'a"  ("(_\<^sup>2)" [1000] 999)
+  where "x\<^sup>2 \<equiv> x ^ 2"
 
 end
 

--- a/src/HOL/Product_Type.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Product_Type.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -226,11 +226,11 @@
 
 definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}"
 
-typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
+typedef ('a, 'b) prod ("(_ \<times>/ _)" [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
   unfolding prod_def by auto
 
-type_notation (xsymbols)
-  "prod"  ("(_ \<times>/ _)" [21, 20] 20)
+type_notation (ASCII)
+  prod  (infixr "*" 20)
 
 definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
   "Pair a b = Abs_prod (Pair_Rep a b)"

--- a/src/HOL/Record.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Record.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -427,26 +427,26 @@
   "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")
   ""                    :: "field_type => field_types"          ("_")
   "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")
-  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
-  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
+  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
+  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
 
   "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
   ""                    :: "field => fields"                    ("_")
   "_fields"             :: "field => fields => fields"          ("_,/ _")
-  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
-  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
+  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
+  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
 
   "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
   ""                    :: "field_update => field_updates"      ("_")
   "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
-  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
+  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
 
-syntax (xsymbols)
-  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
-  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
-  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
-  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
-  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
+syntax (ASCII)
+  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
+  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
+  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
+  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
+  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
 
 
 subsection \<open>Record package\<close>

--- a/src/HOL/Relation.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Relation.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -684,19 +684,17 @@
 
 subsubsection \<open>Converse\<close>
 
-inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_^-1)" [1000] 999)
+inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"  ("(_\<inverse>)" [1000] 999)
   for r :: "('a \<times> 'b) set"
 where
-  "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r^-1"
-
-notation (xsymbols)
-  converse  ("(_\<inverse>)" [1000] 999)
+  "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
 
 notation
-  conversep ("(_^--1)" [1000] 1000)
+  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
 
-notation (xsymbols)
-  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
+notation (ASCII)
+  converse  ("(_^-1)" [1000] 999) and
+  conversep ("(_^--1)" [1000] 1000)
 
 lemma converseI [sym]:
   "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"

--- a/src/HOL/Set.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Set.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -12,41 +12,39 @@
 
 axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" \<comment> "comprehension"
   and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> "membership"
-where
-  mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
+where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
   and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
 
 notation
+  member  ("op \<in>") and
+  member  ("(_/ \<in> _)" [51, 51] 50)
+
+abbreviation not_member
+  where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> "non-membership"
+notation
+  not_member  ("op \<notin>") and
+  not_member  ("(_/ \<notin> _)" [51, 51] 50)
+
+notation (ASCII)
   member  ("op :") and
-  member  ("(_/ : _)" [51, 51] 50)
-
-abbreviation not_member where
-  "not_member x A \<equiv> ~ (x : A)" \<comment> "non-membership"
-
-notation
+  member  ("(_/ : _)" [51, 51] 50) and
   not_member  ("op ~:") and
   not_member  ("(_/ ~: _)" [51, 51] 50)
 
-notation (xsymbols)
-  member      ("op \<in>") and
-  member      ("(_/ \<in> _)" [51, 51] 50) and
-  not_member  ("op \<notin>") and
-  not_member  ("(_/ \<notin> _)" [51, 51] 50)
-
 
 text \<open>Set comprehensions\<close>
 
 syntax
   "_Coll" :: "pttrn => bool => 'a set"    ("(1{_./ _})")
 translations
-  "{x. P}" == "CONST Collect (%x. P)"
-
+  "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
+
+syntax (ASCII)
+  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{_ :/ _./ _})")
 syntax
-  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
-syntax (xsymbols)
-  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
+  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{_ \<in>/ _./ _})")
 translations
-  "{p:A. P}" => "CONST Collect (%p. p:A & P)"
+  "{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
 
 lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
   by simp
@@ -141,21 +139,13 @@
 
 subsection \<open>Subsets and bounded quantifiers\<close>
 
-abbreviation
-  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
-  "subset \<equiv> less"
-
-abbreviation
-  subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
-  "subset_eq \<equiv> less_eq"
-
-notation (output)
-  subset  ("op <") and
-  subset  ("(_/ < _)" [51, 51] 50) and
-  subset_eq  ("op <=") and
-  subset_eq  ("(_/ <= _)" [51, 51] 50)
-
-notation (xsymbols)
+abbreviation subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+  where "subset \<equiv> less"
+
+abbreviation subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
+  where "subset_eq \<equiv> less_eq"
+
+notation
   subset  ("op \<subset>") and
   subset  ("(_/ \<subset> _)" [51, 51] 50) and
   subset_eq  ("op \<subseteq>") and
@@ -169,19 +159,25 @@
   supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   "supset_eq \<equiv> greater_eq"
 
-notation (xsymbols)
+notation
   supset  ("op \<supset>") and
   supset  ("(_/ \<supset> _)" [51, 51] 50) and
   supset_eq  ("op \<supseteq>") and
   supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)
 
+notation (ASCII output)
+  subset  ("op <") and
+  subset  ("(_/ < _)" [51, 51] 50) and
+  subset_eq  ("op <=") and
+  subset_eq  ("(_/ <= _)" [51, 51] 50)
+
 definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   \<comment> "bounded universal quantifiers"
 
 definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
   "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   \<comment> "bounded existential quantifiers"
 
-syntax
+syntax (ASCII)
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
@@ -192,32 +188,25 @@
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
 
-syntax (xsymbols)
+syntax
   "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
   "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
   "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
   "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
 
 translations
-  "ALL x:A. P" == "CONST Ball A (%x. P)"
-  "EX x:A. P" == "CONST Bex A (%x. P)"
-  "EX! x:A. P" => "EX! x. x:A & P"
-  "LEAST x:A. P" => "LEAST x. x:A & P"
-
-syntax (output)
+  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
+  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex A (\<lambda>x. P)"
+  "\<exists>!x\<in>A. P" \<rightharpoonup> "\<exists>!x. x \<in> A \<and> P"
+  "LEAST x:A. P" \<rightharpoonup> "LEAST x. x \<in> A \<and> P"
+
+syntax (ASCII output)
   "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
   "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
   "_setleEx1"   :: "[idt, 'a, bool] => bool"  ("(3EX! _<=_./ _)" [0, 0, 10] 10)
 
-syntax (xsymbols)
-  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
-  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
-  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
-  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
-  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
-
 syntax (HOL output)
   "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
   "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
@@ -225,12 +214,19 @@
   "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
   "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)
 
+syntax
+  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
+  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
+  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
+  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
+  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
+
 translations
- "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
- "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
- "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"
- "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
- "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
+ "\<forall>A\<subset>B. P"   \<rightharpoonup>  "\<forall>A. A \<subset> B \<longrightarrow> P"
+ "\<exists>A\<subset>B. P"   \<rightharpoonup>  "\<exists>A. A \<subset> B \<and> P"
+ "\<forall>A\<subseteq>B. P"   \<rightharpoonup>  "\<forall>A. A \<subseteq> B \<longrightarrow> P"
+ "\<exists>A\<subseteq>B. P"   \<rightharpoonup>  "\<exists>A. A \<subseteq> B \<and> P"
+ "\<exists>!A\<subseteq>B. P"  \<rightharpoonup>  "\<exists>!A. A \<subseteq> B \<and> P"
 
 print_translation \<open>
   let
@@ -669,11 +665,11 @@
 
 subsubsection \<open>Binary intersection\<close>
 
-abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
-  "op Int \<equiv> inf"
-
-notation (xsymbols)
-  inter  (infixl "\<inter>" 70)
+abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<inter>" 70)
+  where "op \<inter> \<equiv> inf"
+
+notation (ASCII)
+  inter  (infixl "Int" 70)
 
 lemma Int_def:
   "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
@@ -700,11 +696,11 @@
 
 subsubsection \<open>Binary union\<close>
 
-abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
-  "union \<equiv> sup"
-
-notation (xsymbols)
-  union  (infixl "\<union>" 65)
+abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<union>" 65)
+  where "union \<equiv> sup"
+
+notation (ASCII)
+  union  (infixl "Un" 65)
 
 lemma Un_def:
   "A \<union> B = {x. x \<in> A \<or> x \<in> B}"

--- a/src/HOL/Set_Interval.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Set_Interval.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -59,29 +59,29 @@
 nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
 @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well.\<close>
 
-syntax
+syntax (ASCII)
   "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" [0, 0, 10] 10)
   "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" [0, 0, 10] 10)
   "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" [0, 0, 10] 10)
   "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
 
-syntax (xsymbols)
-  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
-  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_<_./ _)" [0, 0, 10] 10)
-  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
-  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
-
 syntax (latex output)
   "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
   "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10)
   "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10)
   "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
 
+syntax
+  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
+  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_<_./ _)" [0, 0, 10] 10)
+  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
+  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
+
 translations
-  "UN i<=n. A"  == "UN i:{..n}. A"
-  "UN i<n. A"   == "UN i:{..<n}. A"
-  "INT i<=n. A" == "INT i:{..n}. A"
-  "INT i<n. A"  == "INT i:{..<n}. A"
+  "\<Union>i\<le>n. A" \<rightleftharpoons> "\<Union>i\<in>{..n}. A"
+  "\<Union>i<n. A" \<rightleftharpoons> "\<Union>i\<in>{..<n}. A"
+  "\<Inter>i\<le>n. A" \<rightleftharpoons> "\<Inter>i\<in>{..n}. A"
+  "\<Inter>i<n. A" \<rightleftharpoons> "\<Inter>i\<in>{..<n}. A"
 
 
 subsection \<open>Various equivalences\<close>
@@ -1427,16 +1427,12 @@
 
 subsection \<open>Summation indexed over intervals\<close>
 
-syntax
-  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
-  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
-  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
-  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10)
-syntax (xsymbols)
-  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
-  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
-  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
-  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
+syntax (ASCII)
+  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
+  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(SUM _<_./ _)" [0,0,10] 10)
+  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(SUM _<=_./ _)" [0,0,10] 10)
+
 syntax (latex_sum output)
   "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
@@ -1447,9 +1443,15 @@
   "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
 
+syntax
+  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
+  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_<_./ _)" [0,0,10] 10)
+  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
+
 translations
-  "\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}"
-  "\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}"
+  "\<Sum>x=a..b. t" == "CONST setsum (\<lambda>x. t) {a..b}"
+  "\<Sum>x=a..<b. t" == "CONST setsum (\<lambda>x. t) {a..<b}"
   "\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}"
   "\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}"
 
@@ -1783,18 +1785,15 @@
 lemma sum_diff_distrib: "\<forall>x. Q x \<le> P x  \<Longrightarrow> (\<Sum>x<n. P x) - (\<Sum>x<n. Q x) = (\<Sum>x<n. P x - Q x :: nat)"
   by (subst setsum_subtractf_nat) auto
 
+
 subsection \<open>Products indexed over intervals\<close>
 
-syntax
-  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
-  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
-  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
-  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
-syntax (xsymbols)
-  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
-  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
-  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
-  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+syntax (ASCII)
+  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
+  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _<_./ _)" [0,0,10] 10)
+  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _<=_./ _)" [0,0,10] 10)
+
 syntax (latex_prod output)
   "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
@@ -1805,11 +1804,18 @@
   "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
 
+syntax
+  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
+  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
+  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_<_./ _)" [0,0,10] 10)
+  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
+
 translations
-  "\<Prod>x=a..b. t" == "CONST setprod (%x. t) {a..b}"
-  "\<Prod>x=a..<b. t" == "CONST setprod (%x. t) {a..<b}"
-  "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
-  "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
+  "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST setprod (\<lambda>x. t) {a..b}"
+  "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST setprod (\<lambda>x. t) {a..<b}"
+  "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..n}"
+  "\<Prod>i<n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..<n}"
+
 
 subsection \<open>Transfer setup\<close>
 

--- a/src/HOL/Transitive_Closure.thy	Mon Dec 28 19:23:15 2015 +0100
+++ b/src/HOL/Transitive_Closure.thy	Mon Dec 28 21:47:32 2015 +0100
@@ -24,46 +24,43 @@
   notes [[inductive_defs]]
 begin
 
-inductive_set
-  rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"   ("(_^*)" [1000] 999)
+inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>*)" [1000] 999)
+  for r :: "('a \<times> 'a) set"
+where
+  rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"
+| rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"
+
+inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>+)" [1000] 999)
   for r :: "('a \<times> 'a) set"
 where
-    rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*"
-  | rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
+  r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"
+| trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
 
-inductive_set
-  trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_^+)" [1000] 999)
-  for r :: "('a \<times> 'a) set"
-where
-    r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
-  | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+"
+notation
+  rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
+  tranclp  ("(_\<^sup>+\<^sup>+)" [1000] 1000)
 
-declare rtrancl_def [nitpick_unfold del]
-        rtranclp_def [nitpick_unfold del]
-        trancl_def [nitpick_unfold del]
-        tranclp_def [nitpick_unfold del]
+declare
+  rtrancl_def [nitpick_unfold del]
+  rtranclp_def [nitpick_unfold del]
+  trancl_def [nitpick_unfold del]
+  tranclp_def [nitpick_unfold del]
 
 end
 
-notation
-  rtranclp  ("(_^**)" [1000] 1000) and
-  tranclp  ("(_^++)" [1000] 1000)
+abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>=)" [1000] 999)
+  where "r\<^sup>= \<equiv> r \<union> Id"
 
-abbreviation
-  reflclp :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where
-  "r^== \<equiv> sup r op ="
+abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(_\<^sup>=\<^sup>=)" [1000] 1000)
+  where "r\<^sup>=\<^sup>= \<equiv> sup r op ="
 
-abbreviation
-  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
-  "r^= \<equiv> r \<union> Id"
-
-notation (xsymbols)
-  rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
-  tranclp  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
-  reflclp  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
-  rtrancl  ("(_\<^sup>*)" [1000] 999) and
-  trancl  ("(_\<^sup>+)" [1000] 999) and
-  reflcl  ("(_\<^sup>=)" [1000] 999)
+notation (ASCII)
+  rtrancl  ("(_^*)" [1000] 999) and
+  trancl  ("(_^+)" [1000] 999) and
+  reflcl  ("(_^=)" [1000] 999) and
+  rtranclp  ("(_^**)" [1000] 1000) and
+  tranclp  ("(_^++)" [1000] 1000) and
+  reflclp  ("(_^==)" [1000] 1000)
 
 
 subsection \<open>Reflexive closure\<close>