# HG changeset patch
# User wenzelm
# Date 1444497725 -7200
# Node ID 9f5145281888b637c3cc8e5669821d840356c44e
# Parent  6762c84451385086855dd38354d804258b665176
prefer symbols;

diff -r 6762c8445138 -r 9f5145281888 NEWS
--- a/NEWS	Sat Oct 10 16:40:43 2015 +0200
+++ b/NEWS	Sat Oct 10 19:22:05 2015 +0200
@@ -251,6 +251,16 @@
   type_notation Map.map  (infixr "~=>" 0)
   notation Map.map_comp  (infixl "o'_m" 55)
 
+  type_notation FinFun.finfun ("(_ =>f /_)" [22, 21] 21)
+
+  notation FuncSet.funcset  (infixr "->" 60)
+  notation FuncSet.extensional_funcset  (infixr "->\<^sub>E" 60)
+
+  notation Omega_Words_Fun.conc (infixr "conc" 65)
+
+  notation Preorder.equiv ("op ~~")
+    and Preorder.equiv ("(_/ ~~ _)" [51, 51] 50)
+
 * The alternative notation "\<Colon>" for type and sort constraints has been
 removed: in LaTeX document output it looks the same as "::".
 INCOMPATIBILITY, use plain "::" instead.
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -315,7 +315,7 @@
 context comm_monoid begin
 
 lemma finprod_insert [simp]:
-  "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
+  "[| finite F; a \<notin> F; f \<in> F \<rightarrow> carrier G; f a \<in> carrier G |] ==>
    finprod G f (insert a F) = f a \<otimes> finprod G f F"
   apply (rule trans)
    apply (simp add: finprod_def)
@@ -337,13 +337,13 @@
   case empty show ?case by simp
 next
   case (insert a A)
-  have "(%i. \<one>) \<in> A -> carrier G" by auto
+  have "(%i. \<one>) \<in> A \<rightarrow> carrier G" by auto
   with insert show ?case by simp
 qed simp
 
 lemma finprod_closed [simp]:
   fixes A
-  assumes f: "f \<in> A -> carrier G" 
+  assumes f: "f \<in> A \<rightarrow> carrier G" 
   shows "finprod G f A \<in> carrier G"
 using f
 proof (induct A rule: infinite_finite_induct)
@@ -351,20 +351,20 @@
 next
   case (insert a A)
   then have a: "f a \<in> carrier G" by fast
-  from insert have A: "f \<in> A -> carrier G" by fast
+  from insert have A: "f \<in> A \<rightarrow> carrier G" by fast
   from insert A a show ?case by simp
 qed simp
 
 lemma funcset_Int_left [simp, intro]:
-  "[| f \<in> A -> C; f \<in> B -> C |] ==> f \<in> A Int B -> C"
+  "[| f \<in> A \<rightarrow> C; f \<in> B \<rightarrow> C |] ==> f \<in> A Int B \<rightarrow> C"
   by fast
 
 lemma funcset_Un_left [iff]:
-  "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
+  "(f \<in> A Un B \<rightarrow> C) = (f \<in> A \<rightarrow> C & f \<in> B \<rightarrow> C)"
   by fast
 
 lemma finprod_Un_Int:
-  "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
+  "[| finite A; finite B; g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G |] ==>
      finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
      finprod G g A \<otimes> finprod G g B"
 -- \<open>The reversed orientation looks more natural, but LOOPS as a simprule!\<close>
@@ -373,46 +373,46 @@
 next
   case (insert a A)
   then have a: "g a \<in> carrier G" by fast
-  from insert have A: "g \<in> A -> carrier G" by fast
+  from insert have A: "g \<in> A \<rightarrow> carrier G" by fast
   from insert A a show ?case
     by (simp add: m_ac Int_insert_left insert_absorb Int_mono2) 
 qed
 
 lemma finprod_Un_disjoint:
   "[| finite A; finite B; A Int B = {};
-      g \<in> A -> carrier G; g \<in> B -> carrier G |]
+      g \<in> A \<rightarrow> carrier G; g \<in> B \<rightarrow> carrier G |]
    ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
   apply (subst finprod_Un_Int [symmetric])
       apply auto
   done
 
 lemma finprod_multf:
-  "[| f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
+  "[| f \<in> A \<rightarrow> carrier G; g \<in> A \<rightarrow> carrier G |] ==>
    finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
 proof (induct A rule: infinite_finite_induct)
   case empty show ?case by simp
 next
   case (insert a A) then
-  have fA: "f \<in> A -> carrier G" by fast
+  have fA: "f \<in> A \<rightarrow> carrier G" by fast
   from insert have fa: "f a \<in> carrier G" by fast
-  from insert have gA: "g \<in> A -> carrier G" by fast
+  from insert have gA: "g \<in> A \<rightarrow> carrier G" by fast
   from insert have ga: "g a \<in> carrier G" by fast
-  from insert have fgA: "(%x. f x \<otimes> g x) \<in> A -> carrier G"
+  from insert have fgA: "(%x. f x \<otimes> g x) \<in> A \<rightarrow> carrier G"
     by (simp add: Pi_def)
   show ?case
     by (simp add: insert fA fa gA ga fgA m_ac)
 qed simp
 
 lemma finprod_cong':
-  "[| A = B; g \<in> B -> carrier G;
+  "[| A = B; g \<in> B \<rightarrow> carrier G;
       !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
 proof -
-  assume prems: "A = B" "g \<in> B -> carrier G"
+  assume prems: "A = B" "g \<in> B \<rightarrow> carrier G"
     "!!i. i \<in> B ==> f i = g i"
   show ?thesis
   proof (cases "finite B")
     case True
-    then have "!!A. [| A = B; g \<in> B -> carrier G;
+    then have "!!A. [| A = B; g \<in> B \<rightarrow> carrier G;
       !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
     proof induct
       case empty thus ?case by simp
@@ -427,7 +427,7 @@
       next
         assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
           "g \<in> insert x B \<rightarrow> carrier G"
-        thus "f \<in> B -> carrier G" by fastforce
+        thus "f \<in> B \<rightarrow> carrier G" by fastforce
       next
         assume "x ~: B" "!!i. i \<in> insert x B \<Longrightarrow> f i = g i"
           "g \<in> insert x B \<rightarrow> carrier G"
@@ -445,13 +445,13 @@
 qed
 
 lemma finprod_cong:
-  "[| A = B; f \<in> B -> carrier G = True;
+  "[| A = B; f \<in> B \<rightarrow> carrier G = True;
       !!i. i \<in> B =simp=> f i = g i |] ==> finprod G f A = finprod G g B"
   (* This order of prems is slightly faster (3%) than the last two swapped. *)
   by (rule finprod_cong') (auto simp add: simp_implies_def)
 
 text \<open>Usually, if this rule causes a failed congruence proof error,
-  the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
+  the reason is that the premise @{text "g \<in> B \<rightarrow> carrier G"} cannot be shown.
   Adding @{thm [source] Pi_def} to the simpset is often useful.
   For this reason, @{thm [source] finprod_cong}
   is not added to the simpset by default.
@@ -465,16 +465,16 @@
 context comm_monoid begin
 
 lemma finprod_0 [simp]:
-  "f \<in> {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
+  "f \<in> {0::nat} \<rightarrow> carrier G ==> finprod G f {..0} = f 0"
 by (simp add: Pi_def)
 
 lemma finprod_Suc [simp]:
-  "f \<in> {..Suc n} -> carrier G ==>
+  "f \<in> {..Suc n} \<rightarrow> carrier G ==>
    finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
 by (simp add: Pi_def atMost_Suc)
 
 lemma finprod_Suc2:
-  "f \<in> {..Suc n} -> carrier G ==>
+  "f \<in> {..Suc n} \<rightarrow> carrier G ==>
    finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
 proof (induct n)
   case 0 thus ?case by (simp add: Pi_def)
@@ -483,7 +483,7 @@
 qed
 
 lemma finprod_mult [simp]:
-  "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
+  "[| f \<in> {..n} \<rightarrow> carrier G; g \<in> {..n} \<rightarrow> carrier G |] ==>
      finprod G (%i. f i \<otimes> g i) {..n::nat} =
      finprod G f {..n} \<otimes> finprod G g {..n}"
   by (induct n) (simp_all add: m_ac Pi_def)
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Algebra/Group.thy
--- a/src/HOL/Algebra/Group.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Algebra/Group.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -576,7 +576,7 @@
 definition
   hom :: "_ => _ => ('a => 'b) set" where
   "hom G H =
-    {h. h \<in> carrier G -> carrier H &
+    {h. h \<in> carrier G \<rightarrow> carrier H &
       (\<forall>x \<in> carrier G. \<forall>y \<in> carrier G. h (x \<otimes>\<^bsub>G\<^esub> y) = h x \<otimes>\<^bsub>H\<^esub> h y)}"
 
 lemma (in group) hom_compose:
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Algebra/Ring.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -141,7 +141,7 @@
 
 lemmas finsum_cong = add.finprod_cong
 text \<open>Usually, if this rule causes a failed congruence proof error,
-   the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
+   the reason is that the premise @{text "g \<in> B \<rightarrow> carrier G"} cannot be shown.
    Adding @{thm [source] Pi_def} to the simpset is often useful.\<close>
 
 lemmas finsum_reindex = add.finprod_reindex
@@ -490,7 +490,7 @@
 subsubsection \<open>Sums over Finite Sets\<close>
 
 lemma (in semiring) finsum_ldistr:
-  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
+  "[| finite A; a \<in> carrier R; f \<in> A \<rightarrow> carrier R |] ==>
    finsum R f A \<otimes> a = finsum R (%i. f i \<otimes> a) A"
 proof (induct set: finite)
   case empty then show ?case by simp
@@ -499,7 +499,7 @@
 qed
 
 lemma (in semiring) finsum_rdistr:
-  "[| finite A; a \<in> carrier R; f \<in> A -> carrier R |] ==>
+  "[| finite A; a \<in> carrier R; f \<in> A \<rightarrow> carrier R |] ==>
    a \<otimes> finsum R f A = finsum R (%i. a \<otimes> f i) A"
 proof (induct set: finite)
   case empty then show ?case by simp
@@ -609,7 +609,7 @@
 definition
   ring_hom :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme] => ('a => 'b) set"
   where "ring_hom R S =
-    {h. h \<in> carrier R -> carrier S &
+    {h. h \<in> carrier R \<rightarrow> carrier S &
       (ALL x y. x \<in> carrier R & y \<in> carrier R -->
         h (x \<otimes>\<^bsub>R\<^esub> y) = h x \<otimes>\<^bsub>S\<^esub> h y & h (x \<oplus>\<^bsub>R\<^esub> y) = h x \<oplus>\<^bsub>S\<^esub> h y) &
       h \<one>\<^bsub>R\<^esub> = \<one>\<^bsub>S\<^esub>}"
@@ -675,12 +675,12 @@
 qed
 
 lemma (in ring_hom_cring) hom_finsum [simp]:
-  "f \<in> A -> carrier R ==>
+  "f \<in> A \<rightarrow> carrier R ==>
   h (finsum R f A) = finsum S (h o f) A"
   by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
 
 lemma (in ring_hom_cring) hom_finprod:
-  "f \<in> A -> carrier R ==>
+  "f \<in> A \<rightarrow> carrier R ==>
   h (finprod R f A) = finprod S (h o f) A"
   by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
 
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -54,7 +54,7 @@
 
 definition
   up :: "('a, 'm) ring_scheme => (nat => 'a) set"
-  where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
+  where "up R = {f. f \<in> UNIV \<rightarrow> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
 
 definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
   where "UP R = \<lparr>
@@ -309,8 +309,8 @@
   fix n
   {
     fix k and a b c :: "nat=>'a"
-    assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
-      "c \<in> UNIV -> carrier R"
+    assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
+      "c \<in> UNIV \<rightarrow> carrier R"
     then have "k <= n ==>
       (\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
       (\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
@@ -409,7 +409,7 @@
   fix n
   {
     fix k and a b :: "nat=>'a"
-    assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
+    assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
     then have "k <= n ==>
       (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
       (is "_ \<Longrightarrow> ?eq k")
@@ -956,7 +956,7 @@
 
 lemma coeff_finsum:
   assumes fin: "finite A"
-  shows "p \<in> A -> carrier P ==>
+  shows "p \<in> A \<rightarrow> carrier P ==>
     coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
   using fin by induct (auto simp: Pi_def)
 
@@ -1095,11 +1095,11 @@
 begin
 
 theorem diagonal_sum:
-  "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
+  "[| f \<in> {..n + m::nat} \<rightarrow> carrier R; g \<in> {..n + m} \<rightarrow> carrier R |] ==>
   (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
   (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
 proof -
-  assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
+  assume Rf: "f \<in> {..n + m} \<rightarrow> carrier R" and Rg: "g \<in> {..n + m} \<rightarrow> carrier R"
   {
     fix j
     have "j <= n + m ==>
@@ -1129,7 +1129,7 @@
 
 theorem cauchy_product:
   assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
-    and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
+    and Rf: "f \<in> {..n} \<rightarrow> carrier R" and Rg: "g \<in> {..m} \<rightarrow> carrier R"
   shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
     (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"      (* State reverse direction? *)
 proof -
@@ -1208,7 +1208,7 @@
   maybe it is not that necessary.\<close>
 
 lemma (in ring_hom_ring) hom_finsum [simp]:
-  "f \<in> A -> carrier R ==>
+  "f \<in> A \<rightarrow> carrier R ==>
   h (finsum R f A) = finsum S (h o f) A"
   by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
 
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Library/Extended_Nat.thy
--- a/src/HOL/Library/Extended_Nat.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/Extended_Nat.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -10,10 +10,7 @@
 begin
 
 class infinity =
-  fixes infinity :: "'a"
-
-notation (xsymbols)
-  infinity  ("\<infinity>")
+  fixes infinity :: "'a"  ("\<infinity>")
 
 
 subsection \<open>Type definition\<close>
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Library/FinFun.thy
--- a/src/HOL/Library/FinFun.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/FinFun.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -76,7 +76,7 @@
 
 definition "finfun = {f::'a\<Rightarrow>'b. \<exists>b. finite {a. f a \<noteq> b}}"
 
-typedef ('a,'b) finfun  ("(_ =>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
+typedef ('a,'b) finfun  ("(_ \<Rightarrow>f /_)" [22, 21] 21) = "finfun :: ('a => 'b) set"
   morphisms finfun_apply Abs_finfun
 proof -
   have "\<exists>f. finite {x. f x \<noteq> undefined}"
@@ -1528,9 +1528,6 @@
 text \<open>Deactivate syntax again. Import theory @{text FinFun_Syntax} to reactivate it again\<close>
 
 no_type_notation
-  finfun ("(_ =>f /_)" [22, 21] 21)
-
-no_type_notation (xsymbols)
   finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
 
 no_notation
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Library/FinFun_Syntax.thy
--- a/src/HOL/Library/FinFun_Syntax.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/FinFun_Syntax.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -7,9 +7,6 @@
 begin
 
 type_notation
-  finfun ("(_ =>f /_)" [22, 21] 21)
-
-type_notation (xsymbols)
   finfun ("(_ \<Rightarrow>f /_)" [22, 21] 21)
 
 notation
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Library/FuncSet.thy
--- a/src/HOL/Library/FuncSet.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/FuncSet.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -17,11 +17,8 @@
 definition "restrict" :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a set \<Rightarrow> 'a \<Rightarrow> 'b"
   where "restrict f A = (\<lambda>x. if x \<in> A then f x else undefined)"
 
-abbreviation funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  (infixr "->" 60)
-  where "A -> B \<equiv> Pi A (\<lambda>_. B)"
-
-notation (xsymbols)
-  funcset  (infixr "\<rightarrow>" 60)
+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
   "_Pi"  :: "pttrn \<Rightarrow> 'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set"  ("(3PI _:_./ _)" 10)
@@ -356,11 +353,8 @@
   "_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)"
 
-abbreviation extensional_funcset :: "'a set \<Rightarrow> 'b set \<Rightarrow> ('a \<Rightarrow> 'b) set" (infixr "->\<^sub>E" 60)
-  where "A ->\<^sub>E B \<equiv> (\<Pi>\<^sub>E i\<in>A. B)"
-
-notation (xsymbols)
-  extensional_funcset  (infixr "\<rightarrow>\<^sub>E" 60)
+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)"
 
 lemma extensional_funcset_def: "extensional_funcset S T = (S \<rightarrow> T) \<inter> extensional S"
   by (simp add: PiE_def)
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Library/Omega_Words_Fun.thy
--- a/src/HOL/Library/Omega_Words_Fun.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/Omega_Words_Fun.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -44,17 +44,13 @@
 \<close>
 
 definition
-  conc :: "['a list, 'a word] \<Rightarrow> 'a word"    (infixr "conc" 65)
-  where "w conc x == \<lambda>n. if n < length w then w!n else x (n - length w)"
+  conc :: "['a list, 'a word] \<Rightarrow> 'a word"  (infixr "\<frown>" 65)
+  where "w \<frown> x == \<lambda>n. if n < length w then w!n else x (n - length w)"
 
 definition
-  iter :: "'a list \<Rightarrow> 'a word"
+  iter :: "'a list \<Rightarrow> 'a word"  ("(_\<^sup>\<omega>)" [1000])
   where "iter w == if w = [] then undefined else (\<lambda>n. w!(n mod (length w)))"
 
-notation (xsymbols)
-  conc (infixr "\<frown>" 65) and
-  iter ("(_\<^sup>\<omega>)" [1000])
-
 lemma conc_empty[simp]: "[] \<frown> w = w"
   unfolding conc_def by auto
 
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Library/Preorder.thy
--- a/src/HOL/Library/Preorder.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Library/Preorder.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -13,10 +13,6 @@
   "equiv x y \<longleftrightarrow> x \<le> y \<and> y \<le> x"
 
 notation
-  equiv ("op ~~") and
-  equiv ("(_/ ~~ _)" [51, 51] 50)
-  
-notation (xsymbols)
   equiv ("op \<approx>") and
   equiv ("(_/ \<approx> _)"  [51, 51] 50)
 
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Metis_Examples/Abstraction.thy
--- a/src/HOL/Metis_Examples/Abstraction.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Metis_Examples/Abstraction.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -142,8 +142,8 @@
 by auto
 
 lemma
-  "map (\<lambda>w. (w -> w, w \<times> w)) xs =
-   zip (map (\<lambda>w. w -> w) xs) (map (\<lambda>w. w \<times> w) xs)"
+  "map (\<lambda>w. (w \<rightarrow> w, w \<times> w)) xs =
+   zip (map (\<lambda>w. w \<rightarrow> w) xs) (map (\<lambda>w. w \<times> w) xs)"
 apply (induct xs)
  apply (metis list.map(1) zip_Nil)
 by auto
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Metis_Examples/Tarski.thy
--- a/src/HOL/Metis_Examples/Tarski.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Metis_Examples/Tarski.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -97,7 +97,7 @@
 
 definition CLF_set :: "('a potype * ('a => 'a)) set" where
   "CLF_set = (SIGMA cl: CompleteLattice.
-            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
+            {f. f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)})"
 
 locale CLF = CL +
   fixes f :: "'a => 'a"
@@ -402,7 +402,7 @@
 declare (in CLF) f_cl [simp]
 
 lemma (in CLF) [simp]:
-    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
+    "f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)"
 proof -
   have "\<forall>u v. (v, u) \<in> CLF_set \<longrightarrow> u \<in> {R \<in> pset v \<rightarrow> pset v. monotone R (pset v) (order v)}"
     unfolding CLF_set_def using SigmaE2 by blast
@@ -415,7 +415,7 @@
     using F1 by metis
 qed
 
-lemma (in CLF) f_in_funcset: "f \<in> A -> A"
+lemma (in CLF) f_in_funcset: "f \<in> A \<rightarrow> A"
 by (simp add: A_def)
 
 lemma (in CLF) monotone_f: "monotone f A r"
@@ -904,7 +904,7 @@
 done
 
 
-lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 -> intY1"
+lemma (in Tarski) intY1_func: "(%x: intY1. f x) \<in> intY1 \<rightarrow> intY1"
 apply (rule restrict_in_funcset)
 apply (metis intY1_f_closed restrict_in_funcset)
 done
diff -r 6762c8445138 -r 9f5145281888 src/HOL/Probability/Sigma_Algebra.thy
--- a/src/HOL/Probability/Sigma_Algebra.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/Probability/Sigma_Algebra.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -1697,7 +1697,7 @@
 subsubsection {* Measurable functions *}
 
 definition measurable :: "'a measure \<Rightarrow> 'b measure \<Rightarrow> ('a \<Rightarrow> 'b) set" where
-  "measurable A B = {f \<in> space A -> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
+  "measurable A B = {f \<in> space A \<rightarrow> space B. \<forall>y \<in> sets B. f -` y \<inter> space A \<in> sets A}"
 
 lemma measurableI:
   "(\<And>x. x \<in> space M \<Longrightarrow> f x \<in> space N) \<Longrightarrow> (\<And>A. A \<in> sets N \<Longrightarrow> f -` A \<inter> space M \<in> sets M) \<Longrightarrow>
diff -r 6762c8445138 -r 9f5145281888 src/HOL/ex/Tarski.thy
--- a/src/HOL/ex/Tarski.thy	Sat Oct 10 16:40:43 2015 +0200
+++ b/src/HOL/ex/Tarski.thy	Sat Oct 10 19:22:05 2015 +0200
@@ -84,7 +84,7 @@
 definition
   CLF_set :: "('a potype * ('a => 'a)) set" where
   "CLF_set = (SIGMA cl: CompleteLattice.
-            {f. f: pset cl -> pset cl & monotone f (pset cl) (order cl)})"
+            {f. f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)})"
 
 definition
   induced :: "['a set, ('a * 'a) set] => ('a *'a)set" where
@@ -445,7 +445,7 @@
 \<close>
 
 lemma (in CLF) [simp]:
-    "f: pset cl -> pset cl & monotone f (pset cl) (order cl)"
+    "f: pset cl \<rightarrow> pset cl & monotone f (pset cl) (order cl)"
 apply (insert f_cl)
 apply (simp add: CLF_set_def)
 done
@@ -453,7 +453,7 @@
 declare (in CLF) f_cl [simp]
 
 
-lemma (in CLF) f_in_funcset: "f \<in> A -> A"
+lemma (in CLF) f_in_funcset: "f \<in> A \<rightarrow> A"
 by (simp add: A_def)
 
 lemma (in CLF) monotone_f: "monotone f A r"