former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
authorwenzelm
Mon Dec 28 21:47:32 2015 +0100 (2015-12-28)
changeset 61955e96292f32c3c
parent 61954 1d43f86f48be
child 61956 38b73f7940af
former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII";
NEWS
src/HOL/Complete_Lattices.thy
src/HOL/Filter.thy
src/HOL/Fun.thy
src/HOL/Groups_Big.thy
src/HOL/Groups_List.thy
src/HOL/HOL.thy
src/HOL/Inductive.thy
src/HOL/Library/FinFun.thy
src/HOL/Library/FinFun_Syntax.thy
src/HOL/Library/FuncSet.thy
src/HOL/Library/Groups_Big_Fun.thy
src/HOL/Library/Lattice_Syntax.thy
src/HOL/Library/Monad_Syntax.thy
src/HOL/Library/Multiset.thy
src/HOL/Library/Option_ord.thy
src/HOL/Library/OptionalSugar.thy
src/HOL/Library/State_Monad.thy
src/HOL/List.thy
src/HOL/Main.thy
src/HOL/Map.thy
src/HOL/Orderings.thy
src/HOL/Power.thy
src/HOL/Product_Type.thy
src/HOL/Record.thy
src/HOL/Relation.thy
src/HOL/Set.thy
src/HOL/Set_Interval.thy
src/HOL/Transitive_Closure.thy
     1.1 --- a/NEWS	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/NEWS	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -375,6 +375,11 @@
     1.4  
     1.5  *** HOL ***
     1.6  
     1.7 +* Former "xsymbols" syntax with Isabelle symbols is used by default,
     1.8 +without any special print mode. Important ASCII replacement syntax
     1.9 +remains available under print mode "ASCII", but less important syntax
    1.10 +has been removed (see below).
    1.11 +
    1.12  * Combinator to represent case distinction on products is named "case_prod",
    1.13  uniformly, discontinuing any input aliasses.  Very popular theorem aliasses
    1.14  have been retained.
     2.1 --- a/src/HOL/Complete_Lattices.thy	Mon Dec 28 19:23:15 2015 +0100
     2.2 +++ b/src/HOL/Complete_Lattices.thy	Mon Dec 28 21:47:32 2015 +0100
     2.3 @@ -85,27 +85,27 @@
     2.4    with the plain constant names.
     2.5  \<close>
     2.6  
     2.7 -syntax
     2.8 +syntax (ASCII)
     2.9    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3INF _./ _)" [0, 10] 10)
    2.10    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3INF _:_./ _)" [0, 0, 10] 10)
    2.11    "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3SUP _./ _)" [0, 10] 10)
    2.12    "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3SUP _:_./ _)" [0, 0, 10] 10)
    2.13  
    2.14 -syntax (xsymbols)
    2.15 +syntax
    2.16    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
    2.17    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
    2.18    "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    2.19    "_SUP"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Squnion>_\<in>_./ _)" [0, 0, 10] 10)
    2.20  
    2.21  translations
    2.22 -  "INF x y. B"   == "INF x. INF y. B"
    2.23 -  "INF x. B"     == "CONST INFIMUM CONST UNIV (%x. B)"
    2.24 -  "INF x. B"     == "INF x:CONST UNIV. B"
    2.25 -  "INF x:A. B"   == "CONST INFIMUM A (%x. B)"
    2.26 -  "SUP x y. B"   == "SUP x. SUP y. B"
    2.27 -  "SUP x. B"     == "CONST SUPREMUM CONST UNIV (%x. B)"
    2.28 -  "SUP x. B"     == "SUP x:CONST UNIV. B"
    2.29 -  "SUP x:A. B"   == "CONST SUPREMUM A (%x. B)"
    2.30 +  "\<Sqinter>x y. B"   \<rightleftharpoons> "\<Sqinter>x. \<Sqinter>y. B"
    2.31 +  "\<Sqinter>x. B"     \<rightleftharpoons> "CONST INFIMUM CONST UNIV (\<lambda>x. B)"
    2.32 +  "\<Sqinter>x. B"     \<rightleftharpoons> "\<Sqinter>x \<in> CONST UNIV. B"
    2.33 +  "\<Sqinter>x\<in>A. B"   \<rightleftharpoons> "CONST INFIMUM A (\<lambda>x. B)"
    2.34 +  "\<Squnion>x y. B"   \<rightleftharpoons> "\<Squnion>x. \<Squnion>y. B"
    2.35 +  "\<Squnion>x. B"     \<rightleftharpoons> "CONST SUPREMUM CONST UNIV (\<lambda>x. B)"
    2.36 +  "\<Squnion>x. B"     \<rightleftharpoons> "\<Squnion>x \<in> CONST UNIV. B"
    2.37 +  "\<Squnion>x\<in>A. B"   \<rightleftharpoons> "CONST SUPREMUM A (\<lambda>x. B)"
    2.38  
    2.39  print_translation \<open>
    2.40    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INFIMUM} @{syntax_const "_INF"},
    2.41 @@ -970,31 +970,31 @@
    2.42  
    2.43  subsubsection \<open>Intersections of families\<close>
    2.44  
    2.45 -abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    2.46 -  "INTER \<equiv> INFIMUM"
    2.47 +abbreviation INTER :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    2.48 +  where "INTER \<equiv> INFIMUM"
    2.49  
    2.50  text \<open>
    2.51    Note: must use name @{const INTER} here instead of \<open>INT\<close>
    2.52    to allow the following syntax coexist with the plain constant name.
    2.53  \<close>
    2.54  
    2.55 -syntax
    2.56 -  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3INT _./ _)" [0, 10] 10)
    2.57 -  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
    2.58 -
    2.59 -syntax (xsymbols)
    2.60 -  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
    2.61 -  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
    2.62 +syntax (ASCII)
    2.63 +  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3INT _./ _)" [0, 10] 10)
    2.64 +  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3INT _:_./ _)" [0, 0, 10] 10)
    2.65  
    2.66  syntax (latex output)
    2.67 -  "_INTER1"     :: "pttrns => 'b set => 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    2.68 -  "_INTER"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
    2.69 +  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3\<Inter>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
    2.70 +  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3\<Inter>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
    2.71 +
    2.72 +syntax
    2.73 +  "_INTER1"     :: "pttrns \<Rightarrow> 'b set \<Rightarrow> 'b set"           ("(3\<Inter>_./ _)" [0, 10] 10)
    2.74 +  "_INTER"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> 'b set"  ("(3\<Inter>_\<in>_./ _)" [0, 0, 10] 10)
    2.75  
    2.76  translations
    2.77 -  "INT x y. B"  == "INT x. INT y. B"
    2.78 -  "INT x. B"    == "CONST INTER CONST UNIV (%x. B)"
    2.79 -  "INT x. B"    == "INT x:CONST UNIV. B"
    2.80 -  "INT x:A. B"  == "CONST INTER A (%x. B)"
    2.81 +  "\<Inter>x y. B"  \<rightleftharpoons> "\<Inter>x. \<Inter>y. B"
    2.82 +  "\<Inter>x. B"    \<rightleftharpoons> "CONST INTER CONST UNIV (\<lambda>x. B)"
    2.83 +  "\<Inter>x. B"    \<rightleftharpoons> "\<Inter>x \<in> CONST UNIV. B"
    2.84 +  "\<Inter>x\<in>A. B"  \<rightleftharpoons> "CONST INTER A (\<lambda>x. B)"
    2.85  
    2.86  print_translation \<open>
    2.87    [Syntax_Trans.preserve_binder_abs2_tr' @{const_syntax INTER} @{syntax_const "_INTER"}]
    2.88 @@ -1143,39 +1143,36 @@
    2.89  
    2.90  subsubsection \<open>Unions of families\<close>
    2.91  
    2.92 -abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set" where
    2.93 -  "UNION \<equiv> SUPREMUM"
    2.94 +abbreviation UNION :: "'a set \<Rightarrow> ('a \<Rightarrow> 'b set) \<Rightarrow> 'b set"
    2.95 +  where "UNION \<equiv> SUPREMUM"
    2.96  
    2.97  text \<open>
    2.98    Note: must use name @{const UNION} here instead of \<open>UN\<close>
    2.99    to allow the following syntax coexist with the plain constant name.
   2.100  \<close>
   2.101  
   2.102 -syntax
   2.103 +syntax (ASCII)
   2.104    "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3UN _./ _)" [0, 10] 10)
   2.105    "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3UN _:_./ _)" [0, 0, 10] 10)
   2.106  
   2.107 -syntax (xsymbols)
   2.108 -  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
   2.109 -  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
   2.110 -
   2.111  syntax (latex output)
   2.112    "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>(00\<^bsub>_\<^esub>)/ _)" [0, 10] 10)
   2.113    "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>(00\<^bsub>_\<in>_\<^esub>)/ _)" [0, 0, 10] 10)
   2.114  
   2.115 +syntax
   2.116 +  "_UNION1"     :: "pttrns => 'b set => 'b set"           ("(3\<Union>_./ _)" [0, 10] 10)
   2.117 +  "_UNION"      :: "pttrn => 'a set => 'b set => 'b set"  ("(3\<Union>_\<in>_./ _)" [0, 0, 10] 10)
   2.118 +
   2.119  translations
   2.120 -  "UN x y. B"   == "UN x. UN y. B"
   2.121 -  "UN x. B"     == "CONST UNION CONST UNIV (%x. B)"
   2.122 -  "UN x. B"     == "UN x:CONST UNIV. B"
   2.123 -  "UN x:A. B"   == "CONST UNION A (%x. B)"
   2.124 +  "\<Union>x y. B"   \<rightleftharpoons> "\<Union>x. \<Union>y. B"
   2.125 +  "\<Union>x. B"     \<rightleftharpoons> "CONST UNION CONST UNIV (\<lambda>x. B)"
   2.126 +  "\<Union>x. B"     \<rightleftharpoons> "\<Union>x \<in> CONST UNIV. B"
   2.127 +  "\<Union>x\<in>A. B"   \<rightleftharpoons> "CONST UNION A (\<lambda>x. B)"
   2.128  
   2.129  text \<open>
   2.130 -  Note the difference between ordinary xsymbol syntax of indexed
   2.131 +  Note the difference between ordinary syntax of indexed
   2.132    unions and intersections (e.g.\ \<open>\<Union>a\<^sub>1\<in>A\<^sub>1. B\<close>)
   2.133 -  and their \LaTeX\ rendition: @{term"\<Union>a\<^sub>1\<in>A\<^sub>1. B"}. The
   2.134 -  former does not make the index expression a subscript of the
   2.135 -  union/intersection symbol because this leads to problems with nested
   2.136 -  subscripts in Proof General.
   2.137 +  and their \LaTeX\ rendition: @{term"\<Union>a\<^sub>1\<in>A\<^sub>1. B"}.
   2.138  \<close>
   2.139  
   2.140  print_translation \<open>
     3.1 --- a/src/HOL/Filter.thy	Mon Dec 28 19:23:15 2015 +0100
     3.2 +++ b/src/HOL/Filter.thy	Mon Dec 28 21:47:32 2015 +0100
     3.3 @@ -693,19 +693,20 @@
     3.4  lemma eventually_sequentially_seg: "eventually (\<lambda>n. P (n + k)) sequentially \<longleftrightarrow> eventually P sequentially"
     3.5    using eventually_sequentially_Suc[of "\<lambda>n. P (n + k)" for k] by (induction k) auto
     3.6  
     3.7 -subsection \<open> The cofinite filter \<close>
     3.8 +
     3.9 +subsection \<open>The cofinite filter\<close>
    3.10  
    3.11  definition "cofinite = Abs_filter (\<lambda>P. finite {x. \<not> P x})"
    3.12  
    3.13 -abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "INFM " 10) where
    3.14 -  "Inf_many P \<equiv> frequently P cofinite"
    3.15 +abbreviation Inf_many :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<exists>\<^sub>\<infinity>" 10)
    3.16 +  where "Inf_many P \<equiv> frequently P cofinite"
    3.17  
    3.18 -abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "MOST " 10) where
    3.19 -  "Alm_all P \<equiv> eventually P cofinite"
    3.20 +abbreviation Alm_all :: "('a \<Rightarrow> bool) \<Rightarrow> bool"  (binder "\<forall>\<^sub>\<infinity>" 10)
    3.21 +  where "Alm_all P \<equiv> eventually P cofinite"
    3.22  
    3.23 -notation (xsymbols)
    3.24 -  Inf_many  (binder "\<exists>\<^sub>\<infinity>" 10) and
    3.25 -  Alm_all  (binder "\<forall>\<^sub>\<infinity>" 10)
    3.26 +notation (ASCII)
    3.27 +  Inf_many  (binder "INFM " 10) and
    3.28 +  Alm_all  (binder "MOST " 10)
    3.29  
    3.30  lemma eventually_cofinite: "eventually P cofinite \<longleftrightarrow> finite {x. \<not> P x}"
    3.31    unfolding cofinite_def
     4.1 --- a/src/HOL/Fun.thy	Mon Dec 28 19:23:15 2015 +0100
     4.2 +++ b/src/HOL/Fun.thy	Mon Dec 28 21:47:32 2015 +0100
     4.3 @@ -42,11 +42,11 @@
     4.4  
     4.5  subsection \<open>The Composition Operator \<open>f \<circ> g\<close>\<close>
     4.6  
     4.7 -definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c" (infixl "o" 55) where
     4.8 -  "f o g = (\<lambda>x. f (g x))"
     4.9 +definition comp :: "('b \<Rightarrow> 'c) \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c"  (infixl "\<circ>" 55)
    4.10 +  where "f \<circ> g = (\<lambda>x. f (g x))"
    4.11  
    4.12 -notation (xsymbols)
    4.13 -  comp  (infixl "\<circ>" 55)
    4.14 +notation (ASCII)
    4.15 +  comp  (infixl "o" 55)
    4.16  
    4.17  lemma comp_apply [simp]: "(f o g) x = f (g x)"
    4.18    by (simp add: comp_def)
     5.1 --- a/src/HOL/Groups_Big.thy	Mon Dec 28 19:23:15 2015 +0100
     5.2 +++ b/src/HOL/Groups_Big.thy	Mon Dec 28 21:47:32 2015 +0100
     5.3 @@ -471,35 +471,28 @@
     5.4  defines
     5.5    setsum = setsum.F ..
     5.6  
     5.7 -abbreviation
     5.8 -  Setsum ("\<Sum>_" [1000] 999) where
     5.9 -  "\<Sum>A \<equiv> setsum (%x. x) A"
    5.10 +abbreviation Setsum ("\<Sum>_" [1000] 999)
    5.11 +  where "\<Sum>A \<equiv> setsum (\<lambda>x. x) A"
    5.12  
    5.13  end
    5.14  
    5.15 -text\<open>Now: lot's of fancy syntax. First, @{term "setsum (%x. e) A"} is
    5.16 -written \<open>\<Sum>x\<in>A. e\<close>.\<close>
    5.17 +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>
    5.18  
    5.19 +syntax (ASCII)
    5.20 +  "_setsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(3SUM _:_./ _)" [0, 51, 10] 10)
    5.21  syntax
    5.22 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(3SUM _:_./ _)" [0, 51, 10] 10)
    5.23 -syntax (xsymbols)
    5.24 -  "_setsum" :: "pttrn => 'a set => 'b => 'b::comm_monoid_add"    ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
    5.25 -
    5.26 +  "_setsum" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b::comm_monoid_add"  ("(2\<Sum>_\<in>_./ _)" [0, 51, 10] 10)
    5.27  translations \<comment> \<open>Beware of argument permutation!\<close>
    5.28 -  "SUM i:A. b" == "CONST setsum (%i. b) A"
    5.29 -  "\<Sum>i\<in>A. b" == "CONST setsum (%i. b) A"
    5.30 +  "\<Sum>i\<in>A. b" \<rightleftharpoons> "CONST setsum (\<lambda>i. b) A"
    5.31  
    5.32 -text\<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter
    5.33 - \<open>\<Sum>x|P. e\<close>.\<close>
    5.34 +text \<open>Instead of @{term"\<Sum>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Sum>x|P. e\<close>.\<close>
    5.35  
    5.36 +syntax (ASCII)
    5.37 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(3SUM _ |/ _./ _)" [0, 0, 10] 10)
    5.38  syntax
    5.39 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(3SUM _ |/ _./ _)" [0,0,10] 10)
    5.40 -syntax (xsymbols)
    5.41 -  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Sum>_ | (_)./ _)" [0,0,10] 10)
    5.42 -
    5.43 +  "_qsetsum" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Sum>_ | (_)./ _)" [0, 0, 10] 10)
    5.44  translations
    5.45 -  "SUM x|P. t" => "CONST setsum (%x. t) {x. P}"
    5.46 -  "\<Sum>x|P. t" => "CONST setsum (%x. t) {x. P}"
    5.47 +  "\<Sum>x|P. t" => "CONST setsum (\<lambda>x. t) {x. P}"
    5.48  
    5.49  print_translation \<open>
    5.50  let
    5.51 @@ -1059,26 +1052,21 @@
    5.52  
    5.53  end
    5.54  
    5.55 -syntax
    5.56 +syntax (ASCII)
    5.57    "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(4PROD _:_./ _)" [0, 51, 10] 10)
    5.58 -syntax (xsymbols)
    5.59 +syntax
    5.60    "_setprod" :: "pttrn => 'a set => 'b => 'b::comm_monoid_mult"  ("(2\<Prod>_\<in>_./ _)" [0, 51, 10] 10)
    5.61 -
    5.62  translations \<comment> \<open>Beware of argument permutation!\<close>
    5.63 -  "PROD i:A. b" == "CONST setprod (%i. b) A" 
    5.64 -  "\<Prod>i\<in>A. b" == "CONST setprod (%i. b) A" 
    5.65 +  "\<Prod>i\<in>A. b" == "CONST setprod (\<lambda>i. b) A" 
    5.66  
    5.67 -text\<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter
    5.68 - \<open>\<Prod>x|P. e\<close>.\<close>
    5.69 +text \<open>Instead of @{term"\<Prod>x\<in>{x. P}. e"} we introduce the shorter \<open>\<Prod>x|P. e\<close>.\<close>
    5.70  
    5.71 +syntax (ASCII)
    5.72 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(4PROD _ |/ _./ _)" [0, 0, 10] 10)
    5.73  syntax
    5.74 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(4PROD _ |/ _./ _)" [0,0,10] 10)
    5.75 -syntax (xsymbols)
    5.76 -  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a" ("(2\<Prod>_ | (_)./ _)" [0,0,10] 10)
    5.77 -
    5.78 +  "_qsetprod" :: "pttrn \<Rightarrow> bool \<Rightarrow> 'a \<Rightarrow> 'a"  ("(2\<Prod>_ | (_)./ _)" [0, 0, 10] 10)
    5.79  translations
    5.80 -  "PROD x|P. t" => "CONST setprod (%x. t) {x. P}"
    5.81 -  "\<Prod>x|P. t" => "CONST setprod (%x. t) {x. P}"
    5.82 +  "\<Prod>x|P. t" => "CONST setprod (\<lambda>x. t) {x. P}"
    5.83  
    5.84  context comm_monoid_mult
    5.85  begin
     6.1 --- a/src/HOL/Groups_List.thy	Mon Dec 28 19:23:15 2015 +0100
     6.2 +++ b/src/HOL/Groups_List.thy	Mon Dec 28 21:47:32 2015 +0100
     6.3 @@ -93,15 +93,12 @@
     6.4  end
     6.5  
     6.6  text \<open>Some syntactic sugar for summing a function over a list:\<close>
     6.7 -
     6.8 +syntax (ASCII)
     6.9 +  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
    6.10  syntax
    6.11 -  "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3SUM _<-_. _)" [0, 51, 10] 10)
    6.12 -syntax (xsymbols)
    6.13    "_listsum" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Sum>_\<leftarrow>_. _)" [0, 51, 10] 10)
    6.14 -
    6.15  translations \<comment> \<open>Beware of argument permutation!\<close>
    6.16 -  "SUM x<-xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    6.17 -  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (%x. b) xs)"
    6.18 +  "\<Sum>x\<leftarrow>xs. b" == "CONST listsum (CONST map (\<lambda>x. b) xs)"
    6.19  
    6.20  text \<open>TODO duplicates\<close>
    6.21  lemmas listsum_simps = listsum.Nil listsum.Cons
    6.22 @@ -352,13 +349,11 @@
    6.23  
    6.24  text \<open>Some syntactic sugar:\<close>
    6.25  
    6.26 -syntax
    6.27 +syntax (ASCII)
    6.28    "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3PROD _<-_. _)" [0, 51, 10] 10)
    6.29 -syntax (xsymbols)
    6.30 +syntax
    6.31    "_listprod" :: "pttrn => 'a list => 'b => 'b"    ("(3\<Prod>_\<leftarrow>_. _)" [0, 51, 10] 10)
    6.32 -
    6.33  translations \<comment> \<open>Beware of argument permutation!\<close>
    6.34 -  "PROD x<-xs. b" == "CONST listprod (CONST map (%x. b) xs)"
    6.35 -  "\<Prod>x\<leftarrow>xs. b" == "CONST listprod (CONST map (%x. b) xs)"
    6.36 +  "\<Prod>x\<leftarrow>xs. b" \<rightleftharpoons> "CONST listprod (CONST map (\<lambda>x. b) xs)"
    6.37  
    6.38  end
     7.1 --- a/src/HOL/HOL.thy	Mon Dec 28 19:23:15 2015 +0100
     7.2 +++ b/src/HOL/HOL.thy	Mon Dec 28 21:47:32 2015 +0100
     7.3 @@ -73,48 +73,45 @@
     7.4    Trueprop      :: "bool \<Rightarrow> prop"                   ("(_)" 5)
     7.5  
     7.6  axiomatization
     7.7 -  implies       :: "[bool, bool] \<Rightarrow> bool"           (infixr "-->" 25)  and
     7.8 +  implies       :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<longrightarrow>" 25)  and
     7.9    eq            :: "['a, 'a] \<Rightarrow> bool"               (infixl "=" 50)  and
    7.10    The           :: "('a \<Rightarrow> bool) \<Rightarrow> 'a"
    7.11  
    7.12  consts
    7.13    True          :: bool
    7.14    False         :: bool
    7.15 -  Not           :: "bool \<Rightarrow> bool"                   ("~ _" [40] 40)
    7.16 +  Not           :: "bool \<Rightarrow> bool"                   ("\<not> _" [40] 40)
    7.17  
    7.18 -  conj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "&" 35)
    7.19 -  disj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "|" 30)
    7.20 +  conj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<and>" 35)
    7.21 +  disj          :: "[bool, bool] \<Rightarrow> bool"           (infixr "\<or>" 30)
    7.22  
    7.23 -  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "ALL " 10)
    7.24 -  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "EX " 10)
    7.25 -  Ex1           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "EX! " 10)
    7.26 +  All           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<forall>" 10)
    7.27 +  Ex            :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>" 10)
    7.28 +  Ex1           :: "('a \<Rightarrow> bool) \<Rightarrow> bool"           (binder "\<exists>!" 10)
    7.29  
    7.30  
    7.31  subsubsection \<open>Additional concrete syntax\<close>
    7.32  
    7.33 -notation (output)
    7.34 -  eq  (infix "=" 50)
    7.35 -
    7.36 -abbreviation
    7.37 -  not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "~=" 50) where
    7.38 -  "x ~= y \<equiv> ~ (x = y)"
    7.39 +abbreviation not_equal :: "['a, 'a] \<Rightarrow> bool"  (infixl "\<noteq>" 50)
    7.40 +  where "x \<noteq> y \<equiv> \<not> (x = y)"
    7.41  
    7.42  notation (output)
    7.43 +  eq  (infix "=" 50) and
    7.44 +  not_equal  (infix "\<noteq>" 50)
    7.45 +
    7.46 +notation (ASCII output)
    7.47    not_equal  (infix "~=" 50)
    7.48  
    7.49 -notation (xsymbols)
    7.50 -  Not  ("\<not> _" [40] 40) and
    7.51 -  conj  (infixr "\<and>" 35) and
    7.52 -  disj  (infixr "\<or>" 30) and
    7.53 -  implies  (infixr "\<longrightarrow>" 25) and
    7.54 -  not_equal  (infixl "\<noteq>" 50)
    7.55 -
    7.56 -notation (xsymbols output)
    7.57 -  not_equal  (infix "\<noteq>" 50)
    7.58 +notation (ASCII)
    7.59 +  Not  ("~ _" [40] 40) and
    7.60 +  conj  (infixr "&" 35) and
    7.61 +  disj  (infixr "|" 30) and
    7.62 +  implies  (infixr "-->" 25) and
    7.63 +  not_equal  (infixl "~=" 50)
    7.64  
    7.65  abbreviation (iff)
    7.66 -  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25) where
    7.67 -  "A \<longleftrightarrow> B \<equiv> A = B"
    7.68 +  iff :: "[bool, bool] \<Rightarrow> bool"  (infixr "\<longleftrightarrow>" 25)
    7.69 +  where "A \<longleftrightarrow> B \<equiv> A = B"
    7.70  
    7.71  syntax "_The" :: "[pttrn, bool] \<Rightarrow> 'a"  ("(3THE _./ _)" [0, 10] 10)
    7.72  translations "THE x. P" \<rightleftharpoons> "CONST The (\<lambda>x. P)"
    7.73 @@ -134,16 +131,16 @@
    7.74  nonterminal case_syn and cases_syn
    7.75  syntax
    7.76    "_case_syntax" :: "['a, cases_syn] \<Rightarrow> 'b"  ("(case _ of/ _)" 10)
    7.77 -  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ =>/ _)" 10)
    7.78 +  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
    7.79    "" :: "case_syn \<Rightarrow> cases_syn"  ("_")
    7.80    "_case2" :: "[case_syn, cases_syn] \<Rightarrow> cases_syn"  ("_/ | _")
    7.81 -syntax (xsymbols)
    7.82 -  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ \<Rightarrow>/ _)" 10)
    7.83 +syntax (ASCII)
    7.84 +  "_case1" :: "['a, 'b] \<Rightarrow> case_syn"  ("(2_ =>/ _)" 10)
    7.85  
    7.86 -notation (xsymbols)
    7.87 -  All  (binder "\<forall>" 10) and
    7.88 -  Ex  (binder "\<exists>" 10) and
    7.89 -  Ex1  (binder "\<exists>!" 10)
    7.90 +notation (ASCII)
    7.91 +  All  (binder "ALL " 10) and
    7.92 +  Ex  (binder "EX " 10) and
    7.93 +  Ex1  (binder "EX! " 10)
    7.94  
    7.95  notation (HOL)
    7.96    All  (binder "! " 10) and
     8.1 --- a/src/HOL/Inductive.thy	Mon Dec 28 19:23:15 2015 +0100
     8.2 +++ b/src/HOL/Inductive.thy	Mon Dec 28 21:47:32 2015 +0100
     8.3 @@ -370,13 +370,11 @@
     8.4  ML_file "Tools/BNF/bnf_fp_rec_sugar_util.ML"
     8.5  ML_file "Tools/BNF/bnf_lfp_rec_sugar.ML"
     8.6  
     8.7 -text\<open>Lambda-abstractions with pattern matching:\<close>
     8.8 -
     8.9 +text \<open>Lambda-abstractions with pattern matching:\<close>
    8.10 +syntax (ASCII)
    8.11 +  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(%_)" 10)
    8.12  syntax
    8.13 -  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(%_)" 10)
    8.14 -syntax (xsymbols)
    8.15 -  "_lam_pats_syntax" :: "cases_syn => 'a => 'b"               ("(\<lambda>_)" 10)
    8.16 -
    8.17 +  "_lam_pats_syntax" :: "cases_syn \<Rightarrow> 'a \<Rightarrow> 'b"  ("(\<lambda>_)" 10)
    8.18  parse_translation \<open>
    8.19    let
    8.20      fun fun_tr ctxt [cs] =
     9.1 --- a/src/HOL/Library/FinFun.thy	Mon Dec 28 19:23:15 2015 +0100
     9.2 +++ b/src/HOL/Library/FinFun.thy	Mon Dec 28 21:47:32 2015 +0100
     9.3 @@ -907,10 +907,11 @@
     9.4  
     9.5  subsection \<open>Function composition\<close>
     9.6  
     9.7 -definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b" (infixr "o$" 55)
     9.8 -where [code del]: "g o$ f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
     9.9 +definition finfun_comp :: "('a \<Rightarrow> 'b) \<Rightarrow> 'c \<Rightarrow>f 'a \<Rightarrow> 'c \<Rightarrow>f 'b"  (infixr "\<circ>$" 55)
    9.10 +where [code del]: "g \<circ>$ f  = finfun_rec (\<lambda>b. (K$ g b)) (\<lambda>a b c. c(a $:= g b)) f"
    9.11  
    9.12 -notation (xsymbols) finfun_comp (infixr "\<circ>$" 55)
    9.13 +notation (ASCII)
    9.14 +  finfun_comp (infixr "o$" 55)
    9.15  
    9.16  interpretation finfun_comp_aux: finfun_rec_wf_aux "(\<lambda>b. (K$ g b))" "(\<lambda>a b c. c(a $:= g b))"
    9.17  by(unfold_locales)(auto simp add: finfun_upd_apply intro: finfun_ext)
    9.18 @@ -968,10 +969,11 @@
    9.19    thus ?thesis by(auto simp add: fun_eq_iff)
    9.20  qed
    9.21  
    9.22 -definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c" (infixr "$o" 55)
    9.23 -where [code del]: "g $o f = Abs_finfun (op $ g \<circ> f)"
    9.24 +definition finfun_comp2 :: "'b \<Rightarrow>f 'c \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow>f 'c"  (infixr "$\<circ>" 55)
    9.25 +where [code del]: "g $\<circ> f = Abs_finfun (op $ g \<circ> f)"
    9.26  
    9.27 -notation (xsymbol) finfun_comp2 (infixr "$\<circ>" 55)
    9.28 +notation (ASCII)
    9.29 +  finfun_comp2  (infixr "$o" 55)
    9.30  
    9.31  lemma finfun_comp2_const [code, simp]: "finfun_comp2 (K$ c) f = (K$ c)"
    9.32    including finfun
    9.33 @@ -1534,12 +1536,12 @@
    9.34    finfun_const ("K$/ _" [0] 1) and
    9.35    finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
    9.36    finfun_apply (infixl "$" 999) and
    9.37 -  finfun_comp (infixr "o$" 55) and
    9.38 -  finfun_comp2 (infixr "$o" 55) and
    9.39 +  finfun_comp (infixr "\<circ>$" 55) and
    9.40 +  finfun_comp2 (infixr "$\<circ>" 55) and
    9.41    finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
    9.42  
    9.43 -no_notation (xsymbols) 
    9.44 -  finfun_comp (infixr "\<circ>$" 55) and
    9.45 -  finfun_comp2 (infixr "$\<circ>" 55)
    9.46 +no_notation (ASCII) 
    9.47 +  finfun_comp (infixr "o$" 55) and
    9.48 +  finfun_comp2 (infixr "$o" 55)
    9.49  
    9.50  end
    10.1 --- a/src/HOL/Library/FinFun_Syntax.thy	Mon Dec 28 19:23:15 2015 +0100
    10.2 +++ b/src/HOL/Library/FinFun_Syntax.thy	Mon Dec 28 21:47:32 2015 +0100
    10.3 @@ -13,12 +13,12 @@
    10.4    finfun_const ("K$/ _" [0] 1) and
    10.5    finfun_update ("_'(_ $:= _')" [1000,0,0] 1000) and
    10.6    finfun_apply (infixl "$" 999) and
    10.7 -  finfun_comp (infixr "o$" 55) and
    10.8 -  finfun_comp2 (infixr "$o" 55) and
    10.9 +  finfun_comp (infixr "\<circ>$" 55) and
   10.10 +  finfun_comp2 (infixr "$\<circ>" 55) and
   10.11    finfun_Diag ("(1'($_,/ _$'))" [0, 0] 1000)
   10.12  
   10.13 -notation (xsymbols) 
   10.14 -  finfun_comp (infixr "\<circ>$" 55) and
   10.15 -  finfun_comp2 (infixr "$\<circ>" 55)
   10.16 +notation (ASCII)
   10.17 +  finfun_comp (infixr "o$" 55) and
   10.18 +  finfun_comp2 (infixr "$o" 55)
   10.19  
   10.20  end
   10.21 \ No newline at end of file
    11.1 --- a/src/HOL/Library/FuncSet.thy	Mon Dec 28 19:23:15 2015 +0100
    11.2 +++ b/src/HOL/Library/FuncSet.thy	Mon Dec 28 21:47:32 2015 +0100
    11.3 @@ -20,10 +20,10 @@
    11.4  abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "\<rightarrow>" 60)
    11.5    where "A \<rightarrow> B \<equiv> Pi A (\<lambda>_. B)"
    11.6  
    11.7 -syntax
    11.8 +syntax (ASCII)
    11.9    "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
   11.10    "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3%_:_./ _)" [0,0,3] 3)
   11.11 -syntax (xsymbols)
   11.12 +syntax
   11.13    "_Pi" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi> _\<in>_./ _)"   10)
   11.14    "_lam" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> ('a \<Rightarrow> 'b) \<Rightarrow> ('a \<Rightarrow> 'b)"  ("(3\<lambda>_\<in>_./ _)" [0,0,3] 3)
   11.15  translations
   11.16 @@ -347,11 +347,12 @@
   11.17  
   11.18  abbreviation "Pi\<^sub>E A B \<equiv> PiE A B"
   11.19  
   11.20 -syntax
   11.21 +syntax (ASCII)
   11.22    "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PIE _:_./ _)" 10)
   11.23 -syntax (xsymbols)
   11.24 +syntax
   11.25    "_PiE" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3\<Pi>\<^sub>E _\<in>_./ _)" 10)
   11.26 -translations "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
   11.27 +translations
   11.28 +  "\<Pi>\<^sub>E x\<in>A. B" \<rightleftharpoons> "CONST Pi\<^sub>E A (\<lambda>x. B)"
   11.29  
   11.30  abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "\<rightarrow>\<^sub>E" 60)
   11.31    where "A \<rightarrow>\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
    12.1 --- a/src/HOL/Library/Groups_Big_Fun.thy	Mon Dec 28 19:23:15 2015 +0100
    12.2 +++ b/src/HOL/Library/Groups_Big_Fun.thy	Mon Dec 28 21:47:32 2015 +0100
    12.3 @@ -233,12 +233,12 @@
    12.4  
    12.5  end
    12.6  
    12.7 -syntax
    12.8 +syntax (ASCII)
    12.9    "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3SUM _. _)" [0, 10] 10)
   12.10 -syntax (xsymbols)
   12.11 +syntax
   12.12    "_Sum_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"    ("(3\<Sum>_. _)" [0, 10] 10)
   12.13  translations
   12.14 -  "\<Sum>a. b" == "CONST Sum_any (\<lambda>a. b)"
   12.15 +  "\<Sum>a. b" \<rightleftharpoons> "CONST Sum_any (\<lambda>a. b)"
   12.16  
   12.17  lemma Sum_any_left_distrib:
   12.18    fixes r :: "'a :: semiring_0"
   12.19 @@ -302,10 +302,10 @@
   12.20  
   12.21  end
   12.22  
   12.23 +syntax (ASCII)
   12.24 +  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _. _)" [0, 10] 10)
   12.25  syntax
   12.26 -  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3PROD _. _)" [0, 10] 10)
   12.27 -syntax (xsymbols)
   12.28 -  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"    ("(3\<Prod>_. _)" [0, 10] 10)
   12.29 +  "_Prod_any" :: "pttrn \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_. _)" [0, 10] 10)
   12.30  translations
   12.31    "\<Prod>a. b" == "CONST Prod_any (\<lambda>a. b)"
   12.32  
    13.1 --- a/src/HOL/Library/Lattice_Syntax.thy	Mon Dec 28 19:23:15 2015 +0100
    13.2 +++ b/src/HOL/Library/Lattice_Syntax.thy	Mon Dec 28 21:47:32 2015 +0100
    13.3 @@ -14,7 +14,7 @@
    13.4    Inf  ("\<Sqinter>_" [900] 900) and
    13.5    Sup  ("\<Squnion>_" [900] 900)
    13.6  
    13.7 -syntax (xsymbols)
    13.8 +syntax
    13.9    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   13.10    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   13.11    "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    14.1 --- a/src/HOL/Library/Monad_Syntax.thy	Mon Dec 28 19:23:15 2015 +0100
    14.2 +++ b/src/HOL/Library/Monad_Syntax.thy	Mon Dec 28 21:47:32 2015 +0100
    14.3 @@ -15,42 +15,42 @@
    14.4  \<close>
    14.5  
    14.6  consts
    14.7 -  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr ">>=" 54)
    14.8 +  bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd" (infixr "\<guillemotright>=" 54)
    14.9  
   14.10 -notation (xsymbols)
   14.11 -  bind (infixr "\<guillemotright>=" 54)
   14.12 +notation (ASCII)
   14.13 +  bind (infixr ">>=" 54)
   14.14  
   14.15  notation (latex output)
   14.16    bind (infixr "\<bind>" 54)
   14.17  
   14.18 +
   14.19  abbreviation (do_notation)
   14.20    bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'd"
   14.21 -where
   14.22 -  "bind_do \<equiv> bind"
   14.23 +  where "bind_do \<equiv> bind"
   14.24  
   14.25  notation (output)
   14.26 -  bind_do (infixr ">>=" 54)
   14.27 +  bind_do (infixr "\<guillemotright>=" 54)
   14.28  
   14.29 -notation (xsymbols output)
   14.30 -  bind_do (infixr "\<guillemotright>=" 54)
   14.31 +notation (ASCII output)
   14.32 +  bind_do (infixr ">>=" 54)
   14.33  
   14.34  notation (latex output)
   14.35    bind_do (infixr "\<bind>" 54)
   14.36  
   14.37 +
   14.38  nonterminal do_binds and do_bind
   14.39 -
   14.40  syntax
   14.41    "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
   14.42 -  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
   14.43 +  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
   14.44    "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
   14.45    "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
   14.46    "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
   14.47    "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
   14.48 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
   14.49 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
   14.50  
   14.51 -syntax (xsymbols)
   14.52 -  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
   14.53 -  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<guillemotright>" 54)
   14.54 +syntax (ASCII)
   14.55 +  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
   14.56 +  "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr ">>" 54)
   14.57  
   14.58  syntax (latex output)
   14.59    "_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixr "\<then>" 54)
    15.1 --- a/src/HOL/Library/Multiset.thy	Mon Dec 28 19:23:15 2015 +0100
    15.2 +++ b/src/HOL/Library/Multiset.thy	Mon Dec 28 21:47:32 2015 +0100
    15.3 @@ -25,11 +25,11 @@
    15.4  
    15.5  setup_lifting type_definition_multiset
    15.6  
    15.7 -abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  ("(_/ :# _)" [50, 51] 50) where
    15.8 -  "a :# M == 0 < count M a"
    15.9 -
   15.10 -notation (xsymbols)
   15.11 -  Melem (infix "\<in>#" 50)
   15.12 +abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<in>#" 50)
   15.13 +  where "a \<in># M \<equiv> 0 < count M a"
   15.14 +
   15.15 +notation (ASCII)
   15.16 +  Melem  ("(_/ :# _)" [50, 51] 50)  (* FIXME !? *)
   15.17  
   15.18  lemma multiset_eq_iff: "M = N \<longleftrightarrow> (\<forall>a. count M a = count N a)"
   15.19    by (simp only: count_inject [symmetric] fun_eq_iff)
   15.20 @@ -265,16 +265,18 @@
   15.21  
   15.22  subsubsection \<open>Pointwise ordering induced by count\<close>
   15.23  
   15.24 -definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<=#" 50) where
   15.25 -"subseteq_mset A B = (\<forall>a. count A a \<le> count B a)"
   15.26 -
   15.27 -definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "<#" 50) where
   15.28 -"subset_mset A B = (A <=# B \<and> A \<noteq> B)"
   15.29 -
   15.30 -notation subseteq_mset (infix "\<le>#" 50)
   15.31 -notation (xsymbols) subseteq_mset (infix "\<subseteq>#" 50)
   15.32 -
   15.33 -notation (xsymbols) subset_mset (infix "\<subset>#" 50)
   15.34 +definition subseteq_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<subseteq>#" 50)
   15.35 +  where "A \<subseteq># B = (\<forall>a. count A a \<le> count B a)"
   15.36 +
   15.37 +definition subset_mset :: "'a multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "\<subset>#" 50)
   15.38 +  where "A \<subset># B = (A \<subseteq># B \<and> A \<noteq> B)"
   15.39 +
   15.40 +notation (input)
   15.41 +  subseteq_mset  (infix "\<le>#" 50)
   15.42 +
   15.43 +notation (ASCII)
   15.44 +  subseteq_mset  (infix "<=#" 50) and
   15.45 +  subset_mset  (infix "<#" 50)
   15.46  
   15.47  interpretation subset_mset: ordered_ab_semigroup_add_imp_le "op +" "op -" "op \<subseteq>#" "op \<subset>#"
   15.48    by standard (auto simp add: subset_mset_def subseteq_mset_def multiset_eq_iff intro: order_trans antisym)
   15.49 @@ -504,9 +506,9 @@
   15.50    show ?thesis unfolding B by auto
   15.51  qed
   15.52  
   15.53 -syntax
   15.54 +syntax (ASCII)
   15.55    "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ :# _./ _#})")
   15.56 -syntax (xsymbol)
   15.57 +syntax
   15.58    "_MCollect" :: "pttrn \<Rightarrow> 'a multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"    ("(1{# _ \<in># _./ _#})")
   15.59  translations
   15.60    "{#x \<in># M. P#}" == "CONST filter_mset (\<lambda>x. P) M"
   15.61 @@ -855,27 +857,17 @@
   15.62  lemma image_mset_is_empty_iff [simp]: "image_mset f M = {#} \<longleftrightarrow> M = {#}"
   15.63    by (cases M) auto
   15.64  
   15.65 +syntax (ASCII)
   15.66 +  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ :# _#})")
   15.67  syntax
   15.68 -  "_comprehension1_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
   15.69 -      ("({#_/. _ :# _#})")
   15.70 -translations
   15.71 -  "{#e. x:#M#}" == "CONST image_mset (\<lambda>x. e) M"
   15.72 -
   15.73 -syntax (xsymbols)
   15.74 -  "_comprehension2_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"
   15.75 -      ("({#_/. _ \<in># _#})")
   15.76 +  "_comprehension_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> 'a multiset"  ("({#_/. _ \<in># _#})")
   15.77  translations
   15.78 -  "{#e. x \<in># M#}" == "CONST image_mset (\<lambda>x. e) M"
   15.79 -
   15.80 +  "{#e. x \<in># M#}" \<rightleftharpoons> "CONST image_mset (\<lambda>x. e) M"
   15.81 +
   15.82 +syntax (ASCII)
   15.83 +  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ :# _./ _#})")
   15.84  syntax
   15.85 -  "_comprehension3_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
   15.86 -      ("({#_/ | _ :# _./ _#})")
   15.87 -translations
   15.88 -  "{#e | x:#M. P#}" \<rightharpoonup> "{#e. x :# {# x:#M. P#}#}"
   15.89 -
   15.90 -syntax
   15.91 -  "_comprehension4_mset" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"
   15.92 -      ("({#_/ | _ \<in># _./ _#})")
   15.93 +  "_comprehension_mset'" :: "'a \<Rightarrow> 'b \<Rightarrow> 'b multiset \<Rightarrow> bool \<Rightarrow> 'a multiset"  ("({#_/ | _ \<in># _./ _#})")
   15.94  translations
   15.95    "{#e | x\<in>#M. P#}" \<rightharpoonup> "{#e. x \<in># {# x\<in>#M. P#}#}"
   15.96  
   15.97 @@ -1235,10 +1227,8 @@
   15.98  qed
   15.99  
  15.100  
  15.101 -abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset" where
  15.102 -  "Union_mset MM \<equiv> msetsum MM"
  15.103 -
  15.104 -notation (xsymbols) Union_mset ("\<Union>#_" [900] 900)
  15.105 +abbreviation Union_mset :: "'a multiset multiset \<Rightarrow> 'a multiset"  ("\<Union>#_" [900] 900)
  15.106 +  where "\<Union># MM \<equiv> msetsum MM"
  15.107  
  15.108  lemma set_mset_Union_mset[simp]: "set_mset (\<Union># MM) = (\<Union>M \<in> set_mset MM. set_mset M)"
  15.109    by (induct MM) auto
  15.110 @@ -1246,14 +1236,12 @@
  15.111  lemma in_Union_mset_iff[iff]: "x \<in># \<Union># MM \<longleftrightarrow> (\<exists>M. M \<in># MM \<and> x \<in># M)"
  15.112    by (induct MM) auto
  15.113  
  15.114 +syntax (ASCII)
  15.115 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3SUM _:#_. _)" [0, 51, 10] 10)
  15.116  syntax
  15.117 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
  15.118 -      ("(3SUM _:#_. _)" [0, 51, 10] 10)
  15.119 -syntax (xsymbols)
  15.120 -  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"
  15.121 -      ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
  15.122 +  "_msetsum_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_add"  ("(3\<Sum>_\<in>#_. _)" [0, 51, 10] 10)
  15.123  translations
  15.124 -  "SUM i :# A. b" == "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
  15.125 +  "\<Sum>i \<in># A. b" \<rightleftharpoons> "CONST msetsum (CONST image_mset (\<lambda>i. b) A)"
  15.126  
  15.127  context comm_monoid_mult
  15.128  begin
  15.129 @@ -1287,14 +1275,12 @@
  15.130  
  15.131  end
  15.132  
  15.133 +syntax (ASCII)
  15.134 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3PROD _:#_. _)" [0, 51, 10] 10)
  15.135  syntax
  15.136 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
  15.137 -      ("(3PROD _:#_. _)" [0, 51, 10] 10)
  15.138 -syntax (xsymbols)
  15.139 -  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"
  15.140 -      ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
  15.141 +  "_msetprod_image" :: "pttrn \<Rightarrow> 'b set \<Rightarrow> 'a \<Rightarrow> 'a::comm_monoid_mult"  ("(3\<Prod>_\<in>#_. _)" [0, 51, 10] 10)
  15.142  translations
  15.143 -  "PROD i :# A. b" == "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
  15.144 +  "\<Prod>i \<in># A. b" \<rightleftharpoons> "CONST msetprod (CONST image_mset (\<lambda>i. b) A)"
  15.145  
  15.146  lemma (in comm_semiring_1) dvd_msetprod:
  15.147    assumes "x \<in># A"
  15.148 @@ -1718,14 +1704,15 @@
  15.149  
  15.150  subsubsection \<open>Partial-order properties\<close>
  15.151  
  15.152 -definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<#" 50) where
  15.153 -  "M' #<# M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
  15.154 -
  15.155 -definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool" (infix "#<=#" 50) where
  15.156 -  "M' #<=# M \<longleftrightarrow> M' #<# M \<or> M' = M"
  15.157 -
  15.158 -notation (xsymbols) less_multiset (infix "#\<subset>#" 50)
  15.159 -notation (xsymbols) le_multiset (infix "#\<subseteq>#" 50)
  15.160 +definition less_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "#\<subset>#" 50)
  15.161 +  where "M' #\<subset># M \<longleftrightarrow> (M', M) \<in> mult {(x', x). x' < x}"
  15.162 +
  15.163 +definition le_multiset :: "'a::order multiset \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "#\<subseteq>#" 50)
  15.164 +  where "M' #\<subseteq># M \<longleftrightarrow> M' #\<subset># M \<or> M' = M"
  15.165 +
  15.166 +notation (ASCII)
  15.167 +  less_multiset (infix "#<#" 50) and
  15.168 +  le_multiset (infix "#<=#" 50)
  15.169  
  15.170  interpretation multiset_order: order le_multiset less_multiset
  15.171  proof -
    16.1 --- a/src/HOL/Library/Option_ord.thy	Mon Dec 28 19:23:15 2015 +0100
    16.2 +++ b/src/HOL/Library/Option_ord.thy	Mon Dec 28 21:47:32 2015 +0100
    16.3 @@ -16,7 +16,7 @@
    16.4    Inf  ("\<Sqinter>_" [900] 900) and
    16.5    Sup  ("\<Squnion>_" [900] 900)
    16.6  
    16.7 -syntax (xsymbols)
    16.8 +syntax
    16.9    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   16.10    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   16.11    "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
   16.12 @@ -348,7 +348,7 @@
   16.13    Inf  ("\<Sqinter>_" [900] 900) and
   16.14    Sup  ("\<Squnion>_" [900] 900)
   16.15  
   16.16 -no_syntax (xsymbols)
   16.17 +no_syntax
   16.18    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   16.19    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   16.20    "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    17.1 --- a/src/HOL/Library/OptionalSugar.thy	Mon Dec 28 19:23:15 2015 +0100
    17.2 +++ b/src/HOL/Library/OptionalSugar.thy	Mon Dec 28 21:47:32 2015 +0100
    17.3 @@ -63,7 +63,7 @@
    17.4  
    17.5  (* sorts as intersections *)
    17.6  
    17.7 -syntax (xsymbols output)
    17.8 +syntax (output)
    17.9    "_topsort" :: "sort"  ("\<top>" 1000)
   17.10    "_sort" :: "classes => sort"  ("'(_')" 1000)
   17.11    "_classes" :: "id => classes => classes"  ("_ \<inter> _" 1000)
    18.1 --- a/src/HOL/Library/State_Monad.thy	Mon Dec 28 19:23:15 2015 +0100
    18.2 +++ b/src/HOL/Library/State_Monad.thy	Mon Dec 28 21:47:32 2015 +0100
    18.3 @@ -118,14 +118,14 @@
    18.4  
    18.5  syntax
    18.6    "_sdo_block" :: "sdo_binds \<Rightarrow> 'a" ("exec {//(2  _)//}" [12] 62)
    18.7 -  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
    18.8 +  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
    18.9    "_sdo_let" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(2let _ =/ _)" [1000, 13] 13)
   18.10    "_sdo_then" :: "'a \<Rightarrow> sdo_bind" ("_" [14] 13)
   18.11    "_sdo_final" :: "'a \<Rightarrow> sdo_binds" ("_")
   18.12    "_sdo_cons" :: "[sdo_bind, sdo_binds] \<Rightarrow> sdo_binds" ("_;//_" [13, 12] 12)
   18.13  
   18.14 -syntax (xsymbols)
   18.15 -  "_sdo_bind"  :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ \<leftarrow>/ _)" 13)
   18.16 +syntax (ASCII)
   18.17 +  "_sdo_bind" :: "[pttrn, 'a] \<Rightarrow> sdo_bind" ("(_ <-/ _)" 13)
   18.18  
   18.19  translations
   18.20    "_sdo_block (_sdo_cons (_sdo_bind p t) (_sdo_final e))"
    19.1 --- a/src/HOL/List.thy	Mon Dec 28 19:23:15 2015 +0100
    19.2 +++ b/src/HOL/List.thy	Mon Dec 28 21:47:32 2015 +0100
    19.3 @@ -77,13 +77,13 @@
    19.4  "filter P [] = []" |
    19.5  "filter P (x # xs) = (if P x then x # filter P xs else filter P xs)"
    19.6  
    19.7 +text \<open>Special syntax for filter:\<close>
    19.8 +syntax (ASCII)
    19.9 +  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_<-_./ _])")
   19.10  syntax
   19.11 -  \<comment> \<open>Special syntax for filter\<close>
   19.12 -  "_filter" :: "[pttrn, 'a list, bool] => 'a list"    ("(1[_<-_./ _])")
   19.13 -syntax (xsymbols)
   19.14 -  "_filter" :: "[pttrn, 'a list, bool] => 'a list"("(1[_\<leftarrow>_ ./ _])")
   19.15 +  "_filter" :: "[pttrn, 'a list, bool] => 'a list"  ("(1[_\<leftarrow>_ ./ _])")
   19.16  translations
   19.17 -  "[x<-xs . P]"== "CONST filter (%x. P) xs"
   19.18 +  "[x<-xs . P]" \<rightleftharpoons> "CONST filter (\<lambda>x. P) xs"
   19.19  
   19.20  primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
   19.21  fold_Nil:  "fold f [] = id" |
   19.22 @@ -395,13 +395,16 @@
   19.23  
   19.24  syntax
   19.25    "_listcompr" :: "'a \<Rightarrow> lc_qual \<Rightarrow> lc_quals \<Rightarrow> 'a list"  ("[_ . __")
   19.26 -  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
   19.27 +  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
   19.28    "_lc_test" :: "bool \<Rightarrow> lc_qual" ("_")
   19.29    (*"_lc_let" :: "letbinds => lc_qual"  ("let _")*)
   19.30    "_lc_end" :: "lc_quals" ("]")
   19.31    "_lc_quals" :: "lc_qual \<Rightarrow> lc_quals \<Rightarrow> lc_quals"  (", __")
   19.32    "_lc_abs" :: "'a => 'b list => 'b list"
   19.33  
   19.34 +syntax (ASCII)
   19.35 +  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ <- _")
   19.36 +
   19.37  (* These are easier than ML code but cannot express the optimized
   19.38     translation of [e. p<-xs]
   19.39  translations
   19.40 @@ -415,9 +418,6 @@
   19.41     => "_Let b (_listcompr e Q Qs)"
   19.42  *)
   19.43  
   19.44 -syntax (xsymbols)
   19.45 -  "_lc_gen" :: "'a \<Rightarrow> 'a list \<Rightarrow> lc_qual"  ("_ \<leftarrow> _")
   19.46 -
   19.47  parse_translation \<open>
   19.48    let
   19.49      val NilC = Syntax.const @{const_syntax Nil};
    20.1 --- a/src/HOL/Main.thy	Mon Dec 28 19:23:15 2015 +0100
    20.2 +++ b/src/HOL/Main.thy	Mon Dec 28 21:47:32 2015 +0100
    20.3 @@ -35,7 +35,7 @@
    20.4  
    20.5  hide_fact (open) id_bnf_def type_definition_id_bnf_UNIV
    20.6  
    20.7 -no_syntax (xsymbols)
    20.8 +no_syntax
    20.9    "_INF1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Sqinter>_./ _)" [0, 10] 10)
   20.10    "_INF"      :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sqinter>_\<in>_./ _)" [0, 0, 10] 10)
   20.11    "_SUP1"     :: "pttrns \<Rightarrow> 'b \<Rightarrow> 'b"           ("(3\<Squnion>_./ _)" [0, 10] 10)
    21.1 --- a/src/HOL/Map.thy	Mon Dec 28 19:23:15 2015 +0100
    21.2 +++ b/src/HOL/Map.thy	Mon Dec 28 21:47:32 2015 +0100
    21.3 @@ -47,16 +47,16 @@
    21.4  nonterminal maplets and maplet
    21.5  
    21.6  syntax
    21.7 -  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /|->/ _")
    21.8 -  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[|->]/ _")
    21.9 +  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /\<mapsto>/ _")
   21.10 +  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[\<mapsto>]/ _")
   21.11    ""         :: "maplet \<Rightarrow> maplets"             ("_")
   21.12    "_Maplets" :: "[maplet, maplets] \<Rightarrow> maplets" ("_,/ _")
   21.13 -  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [900,0]900)
   21.14 +  "_MapUpd"  :: "['a \<rightharpoonup> 'b, maplets] \<Rightarrow> 'a \<rightharpoonup> 'b" ("_/'(_')" [900, 0] 900)
   21.15    "_Map"     :: "maplets \<Rightarrow> 'a \<rightharpoonup> 'b"            ("(1[_])")
   21.16  
   21.17 -syntax (xsymbols)
   21.18 -  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /\<mapsto>/ _")
   21.19 -  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[\<mapsto>]/ _")
   21.20 +syntax (ASCII)
   21.21 +  "_maplet"  :: "['a, 'a] \<Rightarrow> maplet"             ("_ /|->/ _")
   21.22 +  "_maplets" :: "['a, 'a] \<Rightarrow> maplet"             ("_ /[|->]/ _")
   21.23  
   21.24  translations
   21.25    "_MapUpd m (_Maplets xy ms)"  \<rightleftharpoons> "_MapUpd (_MapUpd m xy) ms"
   21.26 @@ -65,15 +65,13 @@
   21.27    "_Map (_Maplets ms1 ms2)"     \<leftharpoondown> "_MapUpd (_Map ms1) ms2"
   21.28    "_Maplets ms1 (_Maplets ms2 ms3)" \<leftharpoondown> "_Maplets (_Maplets ms1 ms2) ms3"
   21.29  
   21.30 -primrec
   21.31 -  map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b" where
   21.32 -    "map_of [] = empty"
   21.33 -  | "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
   21.34 +primrec map_of :: "('a \<times> 'b) list \<Rightarrow> 'a \<rightharpoonup> 'b"
   21.35 +where
   21.36 +  "map_of [] = empty"
   21.37 +| "map_of (p # ps) = (map_of ps)(fst p \<mapsto> snd p)"
   21.38  
   21.39 -definition
   21.40 -  map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b" where
   21.41 -  "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
   21.42 -
   21.43 +definition map_upds :: "('a \<rightharpoonup> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b list \<Rightarrow> 'a \<rightharpoonup> 'b"
   21.44 +  where "map_upds m xs ys = m ++ map_of (rev (zip xs ys))"
   21.45  translations
   21.46    "_MapUpd m (_maplets x y)" \<rightleftharpoons> "CONST map_upds m x y"
   21.47  
    22.1 --- a/src/HOL/Orderings.thy	Mon Dec 28 19:23:15 2015 +0100
    22.2 +++ b/src/HOL/Orderings.thy	Mon Dec 28 21:47:32 2015 +0100
    22.3 @@ -93,25 +93,25 @@
    22.4  begin
    22.5  
    22.6  notation
    22.7 -  less_eq  ("op <=") and
    22.8 -  less_eq  ("(_/ <= _)" [51, 51] 50) and
    22.9 +  less_eq  ("op \<le>") and
   22.10 +  less_eq  ("(_/ \<le> _)"  [51, 51] 50) and
   22.11    less  ("op <") and
   22.12    less  ("(_/ < _)"  [51, 51] 50)
   22.13  
   22.14 -notation (xsymbols)
   22.15 -  less_eq  ("op \<le>") and
   22.16 -  less_eq  ("(_/ \<le> _)"  [51, 51] 50)
   22.17 +abbreviation (input)
   22.18 +  greater_eq  (infix "\<ge>" 50)
   22.19 +  where "x \<ge> y \<equiv> y \<le> x"
   22.20  
   22.21  abbreviation (input)
   22.22 -  greater_eq  (infix ">=" 50) where
   22.23 -  "x >= y \<equiv> y <= x"
   22.24 +  greater  (infix ">" 50)
   22.25 +  where "x > y \<equiv> y < x"
   22.26 +
   22.27 +notation (ASCII)
   22.28 +  less_eq  ("op <=") and
   22.29 +  less_eq  ("(_/ <= _)" [51, 51] 50)
   22.30  
   22.31  notation (input)
   22.32 -  greater_eq  (infix "\<ge>" 50)
   22.33 -
   22.34 -abbreviation (input)
   22.35 -  greater  (infix ">" 50) where
   22.36 -  "x > y \<equiv> y < x"
   22.37 +  greater_eq  (infix ">=" 50)
   22.38  
   22.39  end
   22.40  
   22.41 @@ -652,7 +652,7 @@
   22.42  
   22.43  subsection \<open>Bounded quantifiers\<close>
   22.44  
   22.45 -syntax
   22.46 +syntax (ASCII)
   22.47    "_All_less" :: "[idt, 'a, bool] => bool"    ("(3ALL _<_./ _)"  [0, 0, 10] 10)
   22.48    "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3EX _<_./ _)"  [0, 0, 10] 10)
   22.49    "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _<=_./ _)" [0, 0, 10] 10)
   22.50 @@ -663,7 +663,7 @@
   22.51    "_All_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3ALL _>=_./ _)" [0, 0, 10] 10)
   22.52    "_Ex_greater_eq" :: "[idt, 'a, bool] => bool"    ("(3EX _>=_./ _)" [0, 0, 10] 10)
   22.53  
   22.54 -syntax (xsymbols)
   22.55 +syntax
   22.56    "_All_less" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_<_./ _)"  [0, 0, 10] 10)
   22.57    "_Ex_less" :: "[idt, 'a, bool] => bool"    ("(3\<exists>_<_./ _)"  [0, 0, 10] 10)
   22.58    "_All_less_eq" :: "[idt, 'a, bool] => bool"    ("(3\<forall>_\<le>_./ _)" [0, 0, 10] 10)
    23.1 --- a/src/HOL/Power.thy	Mon Dec 28 19:23:15 2015 +0100
    23.2 +++ b/src/HOL/Power.thy	Mon Dec 28 21:47:32 2015 +0100
    23.3 @@ -27,21 +27,17 @@
    23.4  class power = one + times
    23.5  begin
    23.6  
    23.7 -primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a" (infixr "^" 80) where
    23.8 -    power_0: "a ^ 0 = 1"
    23.9 -  | power_Suc: "a ^ Suc n = a * a ^ n"
   23.10 +primrec power :: "'a \<Rightarrow> nat \<Rightarrow> 'a"  (infixr "^" 80)
   23.11 +where
   23.12 +  power_0: "a ^ 0 = 1"
   23.13 +| power_Suc: "a ^ Suc n = a * a ^ n"
   23.14  
   23.15  notation (latex output)
   23.16    power ("(_\<^bsup>_\<^esup>)" [1000] 1000)
   23.17  
   23.18  text \<open>Special syntax for squares.\<close>
   23.19 -
   23.20 -abbreviation (xsymbols)
   23.21 -  power2 :: "'a \<Rightarrow> 'a"  ("(_\<^sup>2)" [1000] 999) where
   23.22 -  "x\<^sup>2 \<equiv> x ^ 2"
   23.23 -
   23.24 -notation (latex output)
   23.25 -  power2  ("(_\<^sup>2)" [1000] 999)
   23.26 +abbreviation power2 :: "'a \<Rightarrow> 'a"  ("(_\<^sup>2)" [1000] 999)
   23.27 +  where "x\<^sup>2 \<equiv> x ^ 2"
   23.28  
   23.29  end
   23.30  
    24.1 --- a/src/HOL/Product_Type.thy	Mon Dec 28 19:23:15 2015 +0100
    24.2 +++ b/src/HOL/Product_Type.thy	Mon Dec 28 21:47:32 2015 +0100
    24.3 @@ -226,11 +226,11 @@
    24.4  
    24.5  definition "prod = {f. \<exists>a b. f = Pair_Rep (a::'a) (b::'b)}"
    24.6  
    24.7 -typedef ('a, 'b) prod (infixr "*" 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
    24.8 +typedef ('a, 'b) prod ("(_ \<times>/ _)" [21, 20] 20) = "prod :: ('a \<Rightarrow> 'b \<Rightarrow> bool) set"
    24.9    unfolding prod_def by auto
   24.10  
   24.11 -type_notation (xsymbols)
   24.12 -  "prod"  ("(_ \<times>/ _)" [21, 20] 20)
   24.13 +type_notation (ASCII)
   24.14 +  prod  (infixr "*" 20)
   24.15  
   24.16  definition Pair :: "'a \<Rightarrow> 'b \<Rightarrow> 'a \<times> 'b" where
   24.17    "Pair a b = Abs_prod (Pair_Rep a b)"
    25.1 --- a/src/HOL/Record.thy	Mon Dec 28 19:23:15 2015 +0100
    25.2 +++ b/src/HOL/Record.thy	Mon Dec 28 21:47:32 2015 +0100
    25.3 @@ -427,26 +427,26 @@
    25.4    "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")
    25.5    ""                    :: "field_type => field_types"          ("_")
    25.6    "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")
    25.7 -  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
    25.8 -  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
    25.9 +  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   25.10 +  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   25.11  
   25.12    "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
   25.13    ""                    :: "field => fields"                    ("_")
   25.14    "_fields"             :: "field => fields => fields"          ("_,/ _")
   25.15 -  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   25.16 -  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   25.17 +  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
   25.18 +  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   25.19  
   25.20    "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
   25.21    ""                    :: "field_update => field_updates"      ("_")
   25.22    "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
   25.23 -  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
   25.24 +  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
   25.25  
   25.26 -syntax (xsymbols)
   25.27 -  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
   25.28 -  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
   25.29 -  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
   25.30 -  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
   25.31 -  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
   25.32 +syntax (ASCII)
   25.33 +  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
   25.34 +  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
   25.35 +  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
   25.36 +  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
   25.37 +  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
   25.38  
   25.39  
   25.40  subsection \<open>Record package\<close>
    26.1 --- a/src/HOL/Relation.thy	Mon Dec 28 19:23:15 2015 +0100
    26.2 +++ b/src/HOL/Relation.thy	Mon Dec 28 21:47:32 2015 +0100
    26.3 @@ -684,19 +684,17 @@
    26.4  
    26.5  subsubsection \<open>Converse\<close>
    26.6  
    26.7 -inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set" ("(_^-1)" [1000] 999)
    26.8 +inductive_set converse :: "('a \<times> 'b) set \<Rightarrow> ('b \<times> 'a) set"  ("(_\<inverse>)" [1000] 999)
    26.9    for r :: "('a \<times> 'b) set"
   26.10  where
   26.11 -  "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r^-1"
   26.12 -
   26.13 -notation (xsymbols)
   26.14 -  converse  ("(_\<inverse>)" [1000] 999)
   26.15 +  "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
   26.16  
   26.17  notation
   26.18 -  conversep ("(_^--1)" [1000] 1000)
   26.19 +  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   26.20  
   26.21 -notation (xsymbols)
   26.22 -  conversep  ("(_\<inverse>\<inverse>)" [1000] 1000)
   26.23 +notation (ASCII)
   26.24 +  converse  ("(_^-1)" [1000] 999) and
   26.25 +  conversep ("(_^--1)" [1000] 1000)
   26.26  
   26.27  lemma converseI [sym]:
   26.28    "(a, b) \<in> r \<Longrightarrow> (b, a) \<in> r\<inverse>"
    27.1 --- a/src/HOL/Set.thy	Mon Dec 28 19:23:15 2015 +0100
    27.2 +++ b/src/HOL/Set.thy	Mon Dec 28 21:47:32 2015 +0100
    27.3 @@ -12,41 +12,39 @@
    27.4  
    27.5  axiomatization Collect :: "('a \<Rightarrow> bool) \<Rightarrow> 'a set" \<comment> "comprehension"
    27.6    and member :: "'a \<Rightarrow> 'a set \<Rightarrow> bool" \<comment> "membership"
    27.7 -where
    27.8 -  mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
    27.9 +where mem_Collect_eq [iff, code_unfold]: "member a (Collect P) = P a"
   27.10    and Collect_mem_eq [simp]: "Collect (\<lambda>x. member x A) = A"
   27.11  
   27.12  notation
   27.13 +  member  ("op \<in>") and
   27.14 +  member  ("(_/ \<in> _)" [51, 51] 50)
   27.15 +
   27.16 +abbreviation not_member
   27.17 +  where "not_member x A \<equiv> \<not> (x \<in> A)" \<comment> "non-membership"
   27.18 +notation
   27.19 +  not_member  ("op \<notin>") and
   27.20 +  not_member  ("(_/ \<notin> _)" [51, 51] 50)
   27.21 +
   27.22 +notation (ASCII)
   27.23    member  ("op :") and
   27.24 -  member  ("(_/ : _)" [51, 51] 50)
   27.25 -
   27.26 -abbreviation not_member where
   27.27 -  "not_member x A \<equiv> ~ (x : A)" \<comment> "non-membership"
   27.28 -
   27.29 -notation
   27.30 +  member  ("(_/ : _)" [51, 51] 50) and
   27.31    not_member  ("op ~:") and
   27.32    not_member  ("(_/ ~: _)" [51, 51] 50)
   27.33  
   27.34 -notation (xsymbols)
   27.35 -  member      ("op \<in>") and
   27.36 -  member      ("(_/ \<in> _)" [51, 51] 50) and
   27.37 -  not_member  ("op \<notin>") and
   27.38 -  not_member  ("(_/ \<notin> _)" [51, 51] 50)
   27.39 -
   27.40  
   27.41  text \<open>Set comprehensions\<close>
   27.42  
   27.43  syntax
   27.44    "_Coll" :: "pttrn => bool => 'a set"    ("(1{_./ _})")
   27.45  translations
   27.46 -  "{x. P}" == "CONST Collect (%x. P)"
   27.47 -
   27.48 +  "{x. P}" \<rightleftharpoons> "CONST Collect (\<lambda>x. P)"
   27.49 +
   27.50 +syntax (ASCII)
   27.51 +  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{_ :/ _./ _})")
   27.52  syntax
   27.53 -  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ :/ _./ _})")
   27.54 -syntax (xsymbols)
   27.55 -  "_Collect" :: "pttrn => 'a set => bool => 'a set"    ("(1{_ \<in>/ _./ _})")
   27.56 +  "_Collect" :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> 'a set"  ("(1{_ \<in>/ _./ _})")
   27.57  translations
   27.58 -  "{p:A. P}" => "CONST Collect (%p. p:A & P)"
   27.59 +  "{p:A. P}" \<rightharpoonup> "CONST Collect (\<lambda>p. p \<in> A \<and> P)"
   27.60  
   27.61  lemma CollectI: "P a \<Longrightarrow> a \<in> {x. P x}"
   27.62    by simp
   27.63 @@ -141,21 +139,13 @@
   27.64  
   27.65  subsection \<open>Subsets and bounded quantifiers\<close>
   27.66  
   27.67 -abbreviation
   27.68 -  subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   27.69 -  "subset \<equiv> less"
   27.70 -
   27.71 -abbreviation
   27.72 -  subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   27.73 -  "subset_eq \<equiv> less_eq"
   27.74 -
   27.75 -notation (output)
   27.76 -  subset  ("op <") and
   27.77 -  subset  ("(_/ < _)" [51, 51] 50) and
   27.78 -  subset_eq  ("op <=") and
   27.79 -  subset_eq  ("(_/ <= _)" [51, 51] 50)
   27.80 -
   27.81 -notation (xsymbols)
   27.82 +abbreviation subset :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   27.83 +  where "subset \<equiv> less"
   27.84 +
   27.85 +abbreviation subset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool"
   27.86 +  where "subset_eq \<equiv> less_eq"
   27.87 +
   27.88 +notation
   27.89    subset  ("op \<subset>") and
   27.90    subset  ("(_/ \<subset> _)" [51, 51] 50) and
   27.91    subset_eq  ("op \<subseteq>") and
   27.92 @@ -169,19 +159,25 @@
   27.93    supset_eq :: "'a set \<Rightarrow> 'a set \<Rightarrow> bool" where
   27.94    "supset_eq \<equiv> greater_eq"
   27.95  
   27.96 -notation (xsymbols)
   27.97 +notation
   27.98    supset  ("op \<supset>") and
   27.99    supset  ("(_/ \<supset> _)" [51, 51] 50) and
  27.100    supset_eq  ("op \<supseteq>") and
  27.101    supset_eq  ("(_/ \<supseteq> _)" [51, 51] 50)
  27.102  
  27.103 +notation (ASCII output)
  27.104 +  subset  ("op <") and
  27.105 +  subset  ("(_/ < _)" [51, 51] 50) and
  27.106 +  subset_eq  ("op <=") and
  27.107 +  subset_eq  ("(_/ <= _)" [51, 51] 50)
  27.108 +
  27.109  definition Ball :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
  27.110    "Ball A P \<longleftrightarrow> (\<forall>x. x \<in> A \<longrightarrow> P x)"   \<comment> "bounded universal quantifiers"
  27.111  
  27.112  definition Bex :: "'a set \<Rightarrow> ('a \<Rightarrow> bool) \<Rightarrow> bool" where
  27.113    "Bex A P \<longleftrightarrow> (\<exists>x. x \<in> A \<and> P x)"   \<comment> "bounded existential quantifiers"
  27.114  
  27.115 -syntax
  27.116 +syntax (ASCII)
  27.117    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3ALL _:_./ _)" [0, 0, 10] 10)
  27.118    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3EX _:_./ _)" [0, 0, 10] 10)
  27.119    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3EX! _:_./ _)" [0, 0, 10] 10)
  27.120 @@ -192,32 +188,25 @@
  27.121    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3? _:_./ _)" [0, 0, 10] 10)
  27.122    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3?! _:_./ _)" [0, 0, 10] 10)
  27.123  
  27.124 -syntax (xsymbols)
  27.125 +syntax
  27.126    "_Ball"       :: "pttrn => 'a set => bool => bool"      ("(3\<forall>_\<in>_./ _)" [0, 0, 10] 10)
  27.127    "_Bex"        :: "pttrn => 'a set => bool => bool"      ("(3\<exists>_\<in>_./ _)" [0, 0, 10] 10)
  27.128    "_Bex1"       :: "pttrn => 'a set => bool => bool"      ("(3\<exists>!_\<in>_./ _)" [0, 0, 10] 10)
  27.129    "_Bleast"     :: "id => 'a set => bool => 'a"           ("(3LEAST_\<in>_./ _)" [0, 0, 10] 10)
  27.130  
  27.131  translations
  27.132 -  "ALL x:A. P" == "CONST Ball A (%x. P)"
  27.133 -  "EX x:A. P" == "CONST Bex A (%x. P)"
  27.134 -  "EX! x:A. P" => "EX! x. x:A & P"
  27.135 -  "LEAST x:A. P" => "LEAST x. x:A & P"
  27.136 -
  27.137 -syntax (output)
  27.138 +  "\<forall>x\<in>A. P" \<rightleftharpoons> "CONST Ball A (\<lambda>x. P)"
  27.139 +  "\<exists>x\<in>A. P" \<rightleftharpoons> "CONST Bex A (\<lambda>x. P)"
  27.140 +  "\<exists>!x\<in>A. P" \<rightharpoonup> "\<exists>!x. x \<in> A \<and> P"
  27.141 +  "LEAST x:A. P" \<rightharpoonup> "LEAST x. x \<in> A \<and> P"
  27.142 +
  27.143 +syntax (ASCII output)
  27.144    "_setlessAll" :: "[idt, 'a, bool] => bool"  ("(3ALL _<_./ _)"  [0, 0, 10] 10)
  27.145    "_setlessEx"  :: "[idt, 'a, bool] => bool"  ("(3EX _<_./ _)"  [0, 0, 10] 10)
  27.146    "_setleAll"   :: "[idt, 'a, bool] => bool"  ("(3ALL _<=_./ _)" [0, 0, 10] 10)
  27.147    "_setleEx"    :: "[idt, 'a, bool] => bool"  ("(3EX _<=_./ _)" [0, 0, 10] 10)
  27.148    "_setleEx1"   :: "[idt, 'a, bool] => bool"  ("(3EX! _<=_./ _)" [0, 0, 10] 10)
  27.149  
  27.150 -syntax (xsymbols)
  27.151 -  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
  27.152 -  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
  27.153 -  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
  27.154 -  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
  27.155 -  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
  27.156 -
  27.157  syntax (HOL output)
  27.158    "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3! _<_./ _)"  [0, 0, 10] 10)
  27.159    "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3? _<_./ _)"  [0, 0, 10] 10)
  27.160 @@ -225,12 +214,19 @@
  27.161    "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3? _<=_./ _)" [0, 0, 10] 10)
  27.162    "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3?! _<=_./ _)" [0, 0, 10] 10)
  27.163  
  27.164 +syntax
  27.165 +  "_setlessAll" :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subset>_./ _)"  [0, 0, 10] 10)
  27.166 +  "_setlessEx"  :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subset>_./ _)"  [0, 0, 10] 10)
  27.167 +  "_setleAll"   :: "[idt, 'a, bool] => bool"   ("(3\<forall>_\<subseteq>_./ _)" [0, 0, 10] 10)
  27.168 +  "_setleEx"    :: "[idt, 'a, bool] => bool"   ("(3\<exists>_\<subseteq>_./ _)" [0, 0, 10] 10)
  27.169 +  "_setleEx1"   :: "[idt, 'a, bool] => bool"   ("(3\<exists>!_\<subseteq>_./ _)" [0, 0, 10] 10)
  27.170 +
  27.171  translations
  27.172 - "\<forall>A\<subset>B. P"   =>  "ALL A. A \<subset> B --> P"
  27.173 - "\<exists>A\<subset>B. P"   =>  "EX A. A \<subset> B & P"
  27.174 - "\<forall>A\<subseteq>B. P"   =>  "ALL A. A \<subseteq> B --> P"
  27.175 - "\<exists>A\<subseteq>B. P"   =>  "EX A. A \<subseteq> B & P"
  27.176 - "\<exists>!A\<subseteq>B. P"  =>  "EX! A. A \<subseteq> B & P"
  27.177 + "\<forall>A\<subset>B. P"   \<rightharpoonup>  "\<forall>A. A \<subset> B \<longrightarrow> P"
  27.178 + "\<exists>A\<subset>B. P"   \<rightharpoonup>  "\<exists>A. A \<subset> B \<and> P"
  27.179 + "\<forall>A\<subseteq>B. P"   \<rightharpoonup>  "\<forall>A. A \<subseteq> B \<longrightarrow> P"
  27.180 + "\<exists>A\<subseteq>B. P"   \<rightharpoonup>  "\<exists>A. A \<subseteq> B \<and> P"
  27.181 + "\<exists>!A\<subseteq>B. P"  \<rightharpoonup>  "\<exists>!A. A \<subseteq> B \<and> P"
  27.182  
  27.183  print_translation \<open>
  27.184    let
  27.185 @@ -669,11 +665,11 @@
  27.186  
  27.187  subsubsection \<open>Binary intersection\<close>
  27.188  
  27.189 -abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Int" 70) where
  27.190 -  "op Int \<equiv> inf"
  27.191 -
  27.192 -notation (xsymbols)
  27.193 -  inter  (infixl "\<inter>" 70)
  27.194 +abbreviation inter :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<inter>" 70)
  27.195 +  where "op \<inter> \<equiv> inf"
  27.196 +
  27.197 +notation (ASCII)
  27.198 +  inter  (infixl "Int" 70)
  27.199  
  27.200  lemma Int_def:
  27.201    "A \<inter> B = {x. x \<in> A \<and> x \<in> B}"
  27.202 @@ -700,11 +696,11 @@
  27.203  
  27.204  subsubsection \<open>Binary union\<close>
  27.205  
  27.206 -abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set" (infixl "Un" 65) where
  27.207 -  "union \<equiv> sup"
  27.208 -
  27.209 -notation (xsymbols)
  27.210 -  union  (infixl "\<union>" 65)
  27.211 +abbreviation union :: "'a set \<Rightarrow> 'a set \<Rightarrow> 'a set"  (infixl "\<union>" 65)
  27.212 +  where "union \<equiv> sup"
  27.213 +
  27.214 +notation (ASCII)
  27.215 +  union  (infixl "Un" 65)
  27.216  
  27.217  lemma Un_def:
  27.218    "A \<union> B = {x. x \<in> A \<or> x \<in> B}"
    28.1 --- a/src/HOL/Set_Interval.thy	Mon Dec 28 19:23:15 2015 +0100
    28.2 +++ b/src/HOL/Set_Interval.thy	Mon Dec 28 21:47:32 2015 +0100
    28.3 @@ -59,29 +59,29 @@
    28.4  nat}: it is equivalent to @{term"{0::nat..<n}"} but some lemmas involving
    28.5  @{term"{m..<n}"} may not exist in @{term"{..<n}"}-form as well.\<close>
    28.6  
    28.7 -syntax
    28.8 +syntax (ASCII)
    28.9    "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3UN _<=_./ _)" [0, 0, 10] 10)
   28.10    "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3UN _<_./ _)" [0, 0, 10] 10)
   28.11    "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3INT _<=_./ _)" [0, 0, 10] 10)
   28.12    "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3INT _<_./ _)" [0, 0, 10] 10)
   28.13  
   28.14 -syntax (xsymbols)
   28.15 -  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
   28.16 -  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_<_./ _)" [0, 0, 10] 10)
   28.17 -  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
   28.18 -  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
   28.19 -
   28.20  syntax (latex output)
   28.21    "_UNION_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ \<le> _)/ _)" [0, 0, 10] 10)
   28.22    "_UNION_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Union>(00_ < _)/ _)" [0, 0, 10] 10)
   28.23    "_INTER_le"   :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ \<le> _)/ _)" [0, 0, 10] 10)
   28.24    "_INTER_less" :: "'a \<Rightarrow> 'a => 'b set => 'b set"       ("(3\<Inter>(00_ < _)/ _)" [0, 0, 10] 10)
   28.25  
   28.26 +syntax
   28.27 +  "_UNION_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_\<le>_./ _)" [0, 0, 10] 10)
   28.28 +  "_UNION_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Union>_<_./ _)" [0, 0, 10] 10)
   28.29 +  "_INTER_le"   :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_\<le>_./ _)" [0, 0, 10] 10)
   28.30 +  "_INTER_less" :: "'a => 'a => 'b set => 'b set"       ("(3\<Inter>_<_./ _)" [0, 0, 10] 10)
   28.31 +
   28.32  translations
   28.33 -  "UN i<=n. A"  == "UN i:{..n}. A"
   28.34 -  "UN i<n. A"   == "UN i:{..<n}. A"
   28.35 -  "INT i<=n. A" == "INT i:{..n}. A"
   28.36 -  "INT i<n. A"  == "INT i:{..<n}. A"
   28.37 +  "\<Union>i\<le>n. A" \<rightleftharpoons> "\<Union>i\<in>{..n}. A"
   28.38 +  "\<Union>i<n. A" \<rightleftharpoons> "\<Union>i\<in>{..<n}. A"
   28.39 +  "\<Inter>i\<le>n. A" \<rightleftharpoons> "\<Inter>i\<in>{..n}. A"
   28.40 +  "\<Inter>i<n. A" \<rightleftharpoons> "\<Inter>i\<in>{..<n}. A"
   28.41  
   28.42  
   28.43  subsection \<open>Various equivalences\<close>
   28.44 @@ -1427,16 +1427,12 @@
   28.45  
   28.46  subsection \<open>Summation indexed over intervals\<close>
   28.47  
   28.48 -syntax
   28.49 -  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
   28.50 -  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
   28.51 -  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<_./ _)" [0,0,10] 10)
   28.52 -  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(SUM _<=_./ _)" [0,0,10] 10)
   28.53 -syntax (xsymbols)
   28.54 -  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
   28.55 -  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
   28.56 -  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_<_./ _)" [0,0,10] 10)
   28.57 -  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
   28.58 +syntax (ASCII)
   28.59 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(SUM _ = _.._./ _)" [0,0,0,10] 10)
   28.60 +  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(SUM _ = _..<_./ _)" [0,0,0,10] 10)
   28.61 +  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(SUM _<_./ _)" [0,0,10] 10)
   28.62 +  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(SUM _<=_./ _)" [0,0,10] 10)
   28.63 +
   28.64  syntax (latex_sum output)
   28.65    "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
   28.66   ("(3\<^raw:$\sum_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
   28.67 @@ -1447,9 +1443,15 @@
   28.68    "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
   28.69   ("(3\<^raw:$\sum_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
   28.70  
   28.71 +syntax
   28.72 +  "_from_to_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_ = _.._./ _)" [0,0,0,10] 10)
   28.73 +  "_from_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_ = _..<_./ _)" [0,0,0,10] 10)
   28.74 +  "_upt_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_<_./ _)" [0,0,10] 10)
   28.75 +  "_upto_setsum" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Sum>_\<le>_./ _)" [0,0,10] 10)
   28.76 +
   28.77  translations
   28.78 -  "\<Sum>x=a..b. t" == "CONST setsum (%x. t) {a..b}"
   28.79 -  "\<Sum>x=a..<b. t" == "CONST setsum (%x. t) {a..<b}"
   28.80 +  "\<Sum>x=a..b. t" == "CONST setsum (\<lambda>x. t) {a..b}"
   28.81 +  "\<Sum>x=a..<b. t" == "CONST setsum (\<lambda>x. t) {a..<b}"
   28.82    "\<Sum>i\<le>n. t" == "CONST setsum (\<lambda>i. t) {..n}"
   28.83    "\<Sum>i<n. t" == "CONST setsum (\<lambda>i. t) {..<n}"
   28.84  
   28.85 @@ -1783,18 +1785,15 @@
   28.86  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)"
   28.87    by (subst setsum_subtractf_nat) auto
   28.88  
   28.89 +
   28.90  subsection \<open>Products indexed over intervals\<close>
   28.91  
   28.92 -syntax
   28.93 -  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
   28.94 -  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
   28.95 -  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<_./ _)" [0,0,10] 10)
   28.96 -  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(PROD _<=_./ _)" [0,0,10] 10)
   28.97 -syntax (xsymbols)
   28.98 -  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
   28.99 -  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
  28.100 -  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_<_./ _)" [0,0,10] 10)
  28.101 -  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b" ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
  28.102 +syntax (ASCII)
  28.103 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _ = _.._./ _)" [0,0,0,10] 10)
  28.104 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _ = _..<_./ _)" [0,0,0,10] 10)
  28.105 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _<_./ _)" [0,0,10] 10)
  28.106 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(PROD _<=_./ _)" [0,0,10] 10)
  28.107 +
  28.108  syntax (latex_prod output)
  28.109    "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  28.110   ("(3\<^raw:$\prod_{>_ = _\<^raw:}^{>_\<^raw:}$> _)" [0,0,0,10] 10)
  28.111 @@ -1805,11 +1804,18 @@
  28.112    "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"
  28.113   ("(3\<^raw:$\prod_{>_ \<le> _\<^raw:}$> _)" [0,0,10] 10)
  28.114  
  28.115 +syntax
  28.116 +  "_from_to_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _.._./ _)" [0,0,0,10] 10)
  28.117 +  "_from_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_ = _..<_./ _)" [0,0,0,10] 10)
  28.118 +  "_upt_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_<_./ _)" [0,0,10] 10)
  28.119 +  "_upto_setprod" :: "idt \<Rightarrow> 'a \<Rightarrow> 'b \<Rightarrow> 'b"  ("(3\<Prod>_\<le>_./ _)" [0,0,10] 10)
  28.120 +
  28.121  translations
  28.122 -  "\<Prod>x=a..b. t" == "CONST setprod (%x. t) {a..b}"
  28.123 -  "\<Prod>x=a..<b. t" == "CONST setprod (%x. t) {a..<b}"
  28.124 -  "\<Prod>i\<le>n. t" == "CONST setprod (\<lambda>i. t) {..n}"
  28.125 -  "\<Prod>i<n. t" == "CONST setprod (\<lambda>i. t) {..<n}"
  28.126 +  "\<Prod>x=a..b. t" \<rightleftharpoons> "CONST setprod (\<lambda>x. t) {a..b}"
  28.127 +  "\<Prod>x=a..<b. t" \<rightleftharpoons> "CONST setprod (\<lambda>x. t) {a..<b}"
  28.128 +  "\<Prod>i\<le>n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..n}"
  28.129 +  "\<Prod>i<n. t" \<rightleftharpoons> "CONST setprod (\<lambda>i. t) {..<n}"
  28.130 +
  28.131  
  28.132  subsection \<open>Transfer setup\<close>
  28.133  
    29.1 --- a/src/HOL/Transitive_Closure.thy	Mon Dec 28 19:23:15 2015 +0100
    29.2 +++ b/src/HOL/Transitive_Closure.thy	Mon Dec 28 21:47:32 2015 +0100
    29.3 @@ -24,46 +24,43 @@
    29.4    notes [[inductive_defs]]
    29.5  begin
    29.6  
    29.7 -inductive_set
    29.8 -  rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"   ("(_^*)" [1000] 999)
    29.9 +inductive_set rtrancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>*)" [1000] 999)
   29.10 +  for r :: "('a \<times> 'a) set"
   29.11 +where
   29.12 +  rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) \<in> r\<^sup>*"
   29.13 +| rtrancl_into_rtrancl [Pure.intro]: "(a, b) \<in> r\<^sup>* \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>*"
   29.14 +
   29.15 +inductive_set trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>+)" [1000] 999)
   29.16    for r :: "('a \<times> 'a) set"
   29.17  where
   29.18 -    rtrancl_refl [intro!, Pure.intro!, simp]: "(a, a) : r^*"
   29.19 -  | rtrancl_into_rtrancl [Pure.intro]: "(a, b) : r^* ==> (b, c) : r ==> (a, c) : r^*"
   29.20 +  r_into_trancl [intro, Pure.intro]: "(a, b) \<in> r \<Longrightarrow> (a, b) \<in> r\<^sup>+"
   29.21 +| trancl_into_trancl [Pure.intro]: "(a, b) \<in> r\<^sup>+ \<Longrightarrow> (b, c) \<in> r \<Longrightarrow> (a, c) \<in> r\<^sup>+"
   29.22  
   29.23 -inductive_set
   29.24 -  trancl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_^+)" [1000] 999)
   29.25 -  for r :: "('a \<times> 'a) set"
   29.26 -where
   29.27 -    r_into_trancl [intro, Pure.intro]: "(a, b) : r ==> (a, b) : r^+"
   29.28 -  | trancl_into_trancl [Pure.intro]: "(a, b) : r^+ ==> (b, c) : r ==> (a, c) : r^+"
   29.29 +notation
   29.30 +  rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
   29.31 +  tranclp  ("(_\<^sup>+\<^sup>+)" [1000] 1000)
   29.32  
   29.33 -declare rtrancl_def [nitpick_unfold del]
   29.34 -        rtranclp_def [nitpick_unfold del]
   29.35 -        trancl_def [nitpick_unfold del]
   29.36 -        tranclp_def [nitpick_unfold del]
   29.37 +declare
   29.38 +  rtrancl_def [nitpick_unfold del]
   29.39 +  rtranclp_def [nitpick_unfold del]
   29.40 +  trancl_def [nitpick_unfold del]
   29.41 +  tranclp_def [nitpick_unfold del]
   29.42  
   29.43  end
   29.44  
   29.45 -notation
   29.46 -  rtranclp  ("(_^**)" [1000] 1000) and
   29.47 -  tranclp  ("(_^++)" [1000] 1000)
   29.48 +abbreviation reflcl :: "('a \<times> 'a) set \<Rightarrow> ('a \<times> 'a) set"  ("(_\<^sup>=)" [1000] 999)
   29.49 +  where "r\<^sup>= \<equiv> r \<union> Id"
   29.50  
   29.51 -abbreviation
   29.52 -  reflclp :: "('a => 'a => bool) => 'a => 'a => bool"  ("(_^==)" [1000] 1000) where
   29.53 -  "r^== \<equiv> sup r op ="
   29.54 +abbreviation reflclp :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a \<Rightarrow> 'a \<Rightarrow> bool"  ("(_\<^sup>=\<^sup>=)" [1000] 1000)
   29.55 +  where "r\<^sup>=\<^sup>= \<equiv> sup r op ="
   29.56  
   29.57 -abbreviation
   29.58 -  reflcl :: "('a \<times> 'a) set => ('a \<times> 'a) set"  ("(_^=)" [1000] 999) where
   29.59 -  "r^= \<equiv> r \<union> Id"
   29.60 -
   29.61 -notation (xsymbols)
   29.62 -  rtranclp  ("(_\<^sup>*\<^sup>*)" [1000] 1000) and
   29.63 -  tranclp  ("(_\<^sup>+\<^sup>+)" [1000] 1000) and
   29.64 -  reflclp  ("(_\<^sup>=\<^sup>=)" [1000] 1000) and
   29.65 -  rtrancl  ("(_\<^sup>*)" [1000] 999) and
   29.66 -  trancl  ("(_\<^sup>+)" [1000] 999) and
   29.67 -  reflcl  ("(_\<^sup>=)" [1000] 999)
   29.68 +notation (ASCII)
   29.69 +  rtrancl  ("(_^*)" [1000] 999) and
   29.70 +  trancl  ("(_^+)" [1000] 999) and
   29.71 +  reflcl  ("(_^=)" [1000] 999) and
   29.72 +  rtranclp  ("(_^**)" [1000] 1000) and
   29.73 +  tranclp  ("(_^++)" [1000] 1000) and
   29.74 +  reflclp  ("(_^==)" [1000] 1000)
   29.75  
   29.76  
   29.77  subsection \<open>Reflexive closure\<close>