diff --git a/library/algebra/complete_lattice.lean b/library/algebra/complete_lattice.lean
index c7f0a70b6..d7e24a56f 100644
--- a/library/algebra/complete_lattice.lean
+++ b/library/algebra/complete_lattice.lean
@@ -125,8 +125,8 @@ variable [C : complete_lattice A]
 include C
 prefix `⨅`:70 := Inf
 prefix `⨆`:65 := Sup
-infix `⊓` := inf
-infix `⊔` := sup
+infix ` ⊓ ` := inf
+infix ` ⊔ ` := sup
 
 variable {f : A → A}
 premise  (mono : ∀ x y : A, x ≤ y → f x ≤ f y)
diff --git a/library/algebra/field.lean b/library/algebra/field.lean
index 5599bad8f..a8cb2a2e0 100644
--- a/library/algebra/field.lean
+++ b/library/algebra/field.lean
@@ -25,7 +25,7 @@ section division_ring
   include s
 
   definition divide (a b : A) : A := a * b⁻¹
-  infix [priority algebra.prio] `/` := divide
+  infix [priority algebra.prio] / := divide
 
   -- only in this file
   local attribute divide [reducible]
diff --git a/library/algebra/group.lean b/library/algebra/group.lean
index d77c2aa2b..df872ecab 100644
--- a/library/algebra/group.lean
+++ b/library/algebra/group.lean
@@ -36,8 +36,8 @@ structure has_inv [class] (A : Type) :=
 structure has_neg [class] (A : Type) :=
 (neg : A → A)
 
-infixl [priority algebra.prio] `*`   := has_mul.mul
-infixl [priority algebra.prio] `+`   := has_add.add
+infixl [priority algebra.prio] ` * `   := has_mul.mul
+infixl [priority algebra.prio] ` + `   := has_add.add
 postfix [priority algebra.prio] `⁻¹` := has_inv.inv
 prefix [priority algebra.prio] `-`   := has_neg.neg
 notation 1  := !has_one.one
@@ -287,8 +287,8 @@ section group
   definition conj_by (g a : A) := g * a * g⁻¹
   definition is_conjugate (a b : A) := ∃ x, conj_by x b = a
 
-  local infixl `~` := is_conjugate
-  local infixr `∘c`:55 := conj_by
+  local infixl ` ~ ` := is_conjugate
+  local infixr ` ∘c `:55 := conj_by
 
   lemma conj_compose (f g a : A) : f ∘c g ∘c a = f*g ∘c a :=
       calc f ∘c g ∘c a = f * (g * a * g⁻¹) * f⁻¹ : rfl
@@ -478,7 +478,7 @@ section add_group
   -- TODO: derive corresponding facts for div in a field
   definition sub [reducible] (a b : A) : A := a + -b
 
-  infix [priority algebra.prio] `-` := sub
+  infix [priority algebra.prio] - := sub
 
   theorem sub_eq_add_neg (a b : A) : a - b = a + -b := rfl
 
diff --git a/library/algebra/group_power.lean b/library/algebra/group_power.lean
index e8c5f1969..fb10d5854 100644
--- a/library/algebra/group_power.lean
+++ b/library/algebra/group_power.lean
@@ -28,7 +28,7 @@ definition pow (a : A) : ℕ → A
 | 0     := 1
 | (n+1) := a * pow n
 
-infix [priority algebra.prio] `^` := pow
+infix [priority algebra.prio] ` ^ ` := pow
 
 theorem pow_zero (a : A) : a^0 = 1 := rfl
 theorem pow_succ (a : A) (n : ℕ) : a^(succ n) = a * a^n := rfl
diff --git a/library/algebra/lattice.lean b/library/algebra/lattice.lean
index b2ec2fb0e..30f70f78e 100644
--- a/library/algebra/lattice.lean
+++ b/library/algebra/lattice.lean
@@ -23,8 +23,8 @@ structure lattice [class] (A : Type) extends weak_order A :=
 
 definition inf := @lattice.inf
 definition sup := @lattice.sup
-infix `⊓`:70 := inf
-infix `⊔`:65 := sup
+infix ` ⊓ `:70 := inf
+infix ` ⊔ `:65 := sup
 
 section
   variable [s : lattice A]
diff --git a/library/algebra/order.lean b/library/algebra/order.lean
index 9f90031a5..017d517a8 100644
--- a/library/algebra/order.lean
+++ b/library/algebra/order.lean
@@ -20,9 +20,9 @@ structure has_le [class] (A : Type) :=
 structure has_lt [class] (A : Type) :=
 (lt : A → A → Prop)
 
-infixl [priority algebra.prio] `<=`  := has_le.le
-infixl [priority algebra.prio] `≤`   := has_le.le
-infixl [priority algebra.prio] `<`   := has_lt.lt
+infixl [priority algebra.prio] <=  := has_le.le
+infixl [priority algebra.prio] ≤   := has_le.le
+infixl [priority algebra.prio] <   := has_lt.lt
 
 definition has_le.ge [reducible] {A : Type} [s : has_le A] (a b : A) := b ≤ a
 notation [priority algebra.prio] a ≥ b := has_le.ge a b
diff --git a/library/data/equiv.lean b/library/data/equiv.lean
index 1523df6e9..509d0ac7e 100644
--- a/library/data/equiv.lean
+++ b/library/data/equiv.lean
@@ -20,12 +20,12 @@ structure equiv [class] (A B : Type) :=
 namespace equiv
 definition perm [reducible] (A : Type) := equiv A A
 
-infix `≃`:50 := equiv
+infix ` ≃ `:50 := equiv
 
 definition fn {A B : Type} (e : equiv A B) : A → B :=
 @equiv.to_fun A B e
 
-infixr `∙`:100 := fn
+infixr ` ∙ `:100 := fn
 
 definition inv {A B : Type} [e : equiv A B] : B → A :=
 @equiv.inv_fun A B e
@@ -54,9 +54,9 @@ protected definition trans [trans] {A B C : Type} : A ≃ B → B ≃ C → A 
 abbreviation id {A : Type} := equiv.refl A
 
 namespace ops
-  postfix `⁻¹` := equiv.symm
-  postfix `⁻¹` := equiv.inv
-  notation e₁ `∘` e₂  := equiv.trans e₂ e₁
+  postfix ⁻¹ := equiv.symm
+  postfix ⁻¹ := equiv.inv
+  notation e₁ ∘ e₂  := equiv.trans e₂ e₁
 end ops
 open equiv.ops
 
diff --git a/library/data/examples/vector.lean b/library/data/examples/vector.lean
index 66ccfdf34..84a284856 100644
--- a/library/data/examples/vector.lean
+++ b/library/data/examples/vector.lean
@@ -15,7 +15,7 @@ inductive vector (A : Type) : nat → Type :=
 
 namespace vector
   notation a :: b := cons a b
-  notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
+  notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
 
   variables {A B C : Type}
 
diff --git a/library/data/finset/basic.lean b/library/data/finset/basic.lean
index 422b19ede..bb186173f 100644
--- a/library/data/finset/basic.lean
+++ b/library/data/finset/basic.lean
@@ -74,7 +74,7 @@ quot.lift_on s (λ l, a ∈ elt_of l)
    (λ ainl₁, mem_perm e ainl₁)
    (λ ainl₂, mem_perm (perm.symm e) ainl₂)))
 
-infix [priority finset.prio] `∈` := mem
+infix [priority finset.prio] ∈ := mem
 notation [priority finset.prio] a ∉ b := ¬ mem a b
 
 theorem mem_of_mem_list {a : A} {l : nodup_list A} : a ∈ elt_of l → a ∈ ⟦l⟧ :=
@@ -169,7 +169,7 @@ quot.lift_on s
   (λ (l₁ l₂ : nodup_list A) (p : l₁ ~ l₂), quot.sound (perm_insert a p))
 
 -- set builder notation
-notation [priority finset.prio] `'{`:max a:(foldr `,` (x b, insert x b) ∅) `}`:0 := a
+notation [priority finset.prio] `'{`:max a:(foldr `, ` (x b, insert x b) ∅) `}`:0 := a
 
 theorem mem_insert (a : A) (s : finset A) : a ∈ insert a s :=
 quot.induction_on s
@@ -546,7 +546,7 @@ quot.lift_on₂ s₁ s₂
     (λ s₁ a i, mem_perm p₂ (s₁ a (mem_perm (perm.symm p₁) i)))
     (λ s₂ a i, mem_perm (perm.symm p₂) (s₂ a (mem_perm p₁ i)))))
 
-infix [priority finset.prio] `⊆` := subset
+infix [priority finset.prio] ⊆ := subset
 
 theorem empty_subset (s : finset A) : ∅ ⊆ s :=
 quot.induction_on s (λ l, list.nil_sub (elt_of l))
diff --git a/library/data/finset/comb.lean b/library/data/finset/comb.lean
index 335800a95..e03d3889d 100644
--- a/library/data/finset/comb.lean
+++ b/library/data/finset/comb.lean
@@ -125,7 +125,7 @@ quot.lift_on s
     (list.nodup_filter p (subtype.has_property l)))
   (λ l₁ l₂ u, quot.sound (perm.perm_filter u))
 
-notation [priority finset.prio] `{` binder ∈ s `|` r:(scoped:1 p, sep p s) `}` := r
+notation [priority finset.prio] `{` binder ` ∈ ` s ` | ` r:(scoped:1 p, sep p s) `}` := r
 
 theorem sep_empty : sep p ∅ = ∅ := rfl
 
@@ -178,7 +178,7 @@ variables {A : Type} [deceq : decidable_eq A]
 include deceq
 
 definition diff (s t : finset A) : finset A := {x ∈ s | x ∉ t}
-infix [priority finset.prio] `\`:70 := diff
+infix [priority finset.prio] ` \ `:70 := diff
 
 theorem mem_of_mem_diff {s t : finset A} {x : A} (H : x ∈ s \ t) : x ∈ s :=
 mem_of_mem_sep H
diff --git a/library/data/hf.lean b/library/data/hf.lean
index f9a3a2b4d..c07956b5b 100644
--- a/library/data/hf.lean
+++ b/library/data/hf.lean
@@ -64,7 +64,7 @@ of_finset (finset.insert a (to_finset s))
 definition mem (a : hf) (s : hf) : Prop :=
 finset.mem a (to_finset s)
 
-infix `∈` := mem
+infix ∈ := mem
 notation [priority finset.prio] a ∉ b := ¬ mem a b
 
 lemma insert_lt_of_not_mem {a s : hf} : a ∉ s → s < insert a s :=
@@ -314,7 +314,7 @@ end
 definition subset (s₁ s₂ : hf) : Prop :=
 finset.subset (to_finset s₁) (to_finset s₂)
 
-infix [priority hf.prio] `⊆` := subset
+infix [priority hf.prio] ⊆ := subset
 
 theorem empty_subset (s : hf) : ∅ ⊆ s :=
 begin unfold [empty, subset], rewrite to_finset_of_finset, apply finset.empty_subset (to_finset s) end
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index 437c9f6cc..550def493 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -45,7 +45,7 @@ namespace int
 
 attribute int.of_nat [coercion]
 
-notation `-[1+` n `]` := int.neg_succ_of_nat n    -- for pretty-printing output
+notation `-[1+ ` n `]` := int.neg_succ_of_nat n    -- for pretty-printing output
 
 /- definitions of basic functions -/
 
@@ -137,7 +137,7 @@ theorem eq_zero_of_nat_abs_eq_zero : Π {a : ℤ}, nat_abs a = 0 → a = 0
 
 protected definition equiv (p q : ℕ × ℕ) : Prop :=  pr1 p + pr2 q = pr2 p + pr1 q
 
-local infix `≡` := int.equiv
+local infix ≡ := int.equiv
 
 protected theorem equiv.refl [refl] {p : ℕ × ℕ} : p ≡ p := !add.comm
 
diff --git a/library/data/int/div.lean b/library/data/int/div.lean
index 3de303d69..5e88ea063 100644
--- a/library/data/int/div.lean
+++ b/library/data/int/div.lean
@@ -26,7 +26,7 @@ notation [priority int.prio] a div b := divide a b
 
 definition modulo (a b : ℤ) : ℤ := a - a div b * b
 notation [priority int.prio] a mod b := modulo a b
-notation [priority int.prio] a `≡` b `[mod`:100 c `]`:0 := a mod c = b mod c
+notation [priority int.prio] a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c
 
 /- div  -/
 
diff --git a/library/data/int/power.lean b/library/data/int/power.lean
index 3dcb7748e..ae522926e 100644
--- a/library/data/int/power.lean
+++ b/library/data/int/power.lean
@@ -19,7 +19,7 @@ section migrate_algebra
   definition pow (a : ℤ) (n : ℕ) : ℤ := algebra.pow a n
   infix [priority int.prio] ^ := pow
   definition nmul (n : ℕ) (a : ℤ) : ℤ := algebra.nmul n a
-  infix [priority int.prio] `⬝` := nmul
+  infix [priority int.prio] ⬝ := nmul
   definition imul (i : ℤ) (a : ℤ) : ℤ := algebra.imul i a
 
   migrate from algebra with int
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 5f6c7b020..90d6b9ee9 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -17,7 +17,7 @@ inhabited.mk list.nil
 
 namespace list
 notation h :: t  := cons h t
-notation `[` l:(foldr `,` (h t, cons h t) nil `]`) := l
+notation `[` l:(foldr `, ` (h t, cons h t) nil `]`) := l
 
 variable {T : Type}
 
@@ -352,7 +352,7 @@ assume P, and.intro (ne_of_not_mem_cons P) (not_mem_of_not_mem_cons P)
 
 definition sublist (l₁ l₂ : list T) := ∀ ⦃a : T⦄, a ∈ l₁ → a ∈ l₂
 
-infix `⊆` := sublist
+infix ⊆ := sublist
 
 theorem nil_sub [simp] (l : list T) : [] ⊆ l :=
 λ b i, false.elim (iff.mp (mem_nil_iff b) i)
diff --git a/library/data/matrix.lean b/library/data/matrix.lean
index bb40ed547..3067891ae 100644
--- a/library/data/matrix.lean
+++ b/library/data/matrix.lean
@@ -17,7 +17,7 @@ definition val [reducible] (M : matrix A m n) (i : fin m) (j : fin n) : A :=
 M i j
 
 namespace ops
-notation M `[` i `,` j `]` := val M i j
+notation M `[` i `, ` j `]` := val M i j
 end ops
 
 open ops
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index f3453ef29..40924c761 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -14,7 +14,7 @@ namespace nat
 
 definition addl (x y : ℕ) : ℕ :=
 nat.rec y (λ n r, succ r) x
-infix `⊕`:65 := addl
+infix ` ⊕ `:65 := addl
 
 theorem addl_succ_right (n m : ℕ) : n ⊕ succ m = succ (n ⊕ m) :=
 nat.induction_on n
diff --git a/library/data/nat/div.lean b/library/data/nat/div.lean
index 9b586565e..211cfa466 100644
--- a/library/data/nat/div.lean
+++ b/library/data/nat/div.lean
@@ -78,7 +78,7 @@ if H : 0 < y ∧ y ≤ x then f (x - y) (div_rec_lemma H) y else x
 
 definition modulo := fix mod.F
 notation a mod b := modulo a b
-notation a `≡` b `[mod`:100 c `]`:0 := a mod c = b mod c
+notation a ≡ b `[mod `:100 c `]`:0 := a mod c = b mod c
 
 theorem modulo_def (x y : nat) : modulo x y = if 0 < y ∧ y ≤ x then modulo (x - y) y else x :=
 congr_fun (fix_eq mod.F x) y
diff --git a/library/data/nat/find.lean b/library/data/nat/find.lean
index 69961e68e..3a9c859e1 100644
--- a/library/data/nat/find.lean
+++ b/library/data/nat/find.lean
@@ -31,7 +31,7 @@ private lemma lbp_succ {x : nat} : lbp x → ¬ p x → lbp (succ x) :=
 private definition gtb (a b : nat) : Prop :=
 a > b ∧ lbp a
 
-local infix `≺`:50 := gtb
+local infix ` ≺ `:50 := gtb
 
 private lemma acc_of_px {x : nat} : p x → acc gtb x :=
 assume h,
diff --git a/library/data/nat/gcd.lean b/library/data/nat/gcd.lean
index f3e07ca5c..f9f6de6d7 100644
--- a/library/data/nat/gcd.lean
+++ b/library/data/nat/gcd.lean
@@ -17,7 +17,7 @@ private definition pair_nat.lt.wf : well_founded pair_nat.lt :=
 intro_k (measure.wf pr₂) 20  -- we use intro_k to be able to execute gcd efficiently in the kernel
 
 local attribute pair_nat.lt.wf [instance]      -- instance will not be saved in .olean
-local infixl `≺`:50 := pair_nat.lt
+local infixl ` ≺ `:50 := pair_nat.lt
 
 private definition gcd.lt.dec (x y₁ : nat) : (succ y₁, x mod succ y₁) ≺ (x, succ y₁) :=
 !mod_lt (succ_pos y₁)
diff --git a/library/data/num.lean b/library/data/num.lean
index 7746fedf3..aee6859ef 100644
--- a/library/data/num.lean
+++ b/library/data/num.lean
@@ -77,7 +77,7 @@ namespace pos_num
     end
 
   local notation a < b         := (lt a b = tt)
-  local notation a `≮`:50 b:50 := (lt a b = ff)
+  local notation a ` ≮ `:50 b:50 := (lt a b = ff)
 
   theorem lt_one_right_eq_ff : ∀ a : pos_num, a ≮ one
   | one      := rfl
diff --git a/library/data/pnat.lean b/library/data/pnat.lean
index 69131888c..0794b55a2 100644
--- a/library/data/pnat.lean
+++ b/library/data/pnat.lean
@@ -27,18 +27,18 @@ theorem pnat_pos (p : ℕ+) : p~ > 0 := has_property p
 
 definition add (p q : ℕ+) : ℕ+ :=
   tag (p~ + q~) (nat.add_pos (pnat_pos p) (pnat_pos q))
-infix `+` := add
+infix + := add
 
 definition mul (p q : ℕ+) : ℕ+ :=
   tag (p~ * q~) (nat.mul_pos (pnat_pos p) (pnat_pos q))
-infix `*` := mul
+infix * := mul
 
 definition le (p q : ℕ+) := p~ ≤ q~
-infix `≤` := le
-notation p `≥` q := q ≤ p
+infix ≤ := le
+notation p ≥ q := q ≤ p
 
 definition lt (p q : ℕ+) := p~ < q~
-infix `<` := lt
+infix < := lt
 
 protected theorem pnat.eq {p q : ℕ+} : p~ = q~ → p = q :=
   subtype.eq
diff --git a/library/data/rat/basic.lean b/library/data/rat/basic.lean
index c51933e0a..b1cea8b2e 100644
--- a/library/data/rat/basic.lean
+++ b/library/data/rat/basic.lean
@@ -22,7 +22,7 @@ namespace prerat
 
 definition equiv (a b : prerat) : Prop := num a * denom b = num b * denom a
 
-infix `≡` := equiv
+infix ≡ := equiv
 
 theorem equiv.refl [refl] (a : prerat) : a ≡ a := rfl
 
@@ -539,12 +539,12 @@ section migrate_algebra
   local attribute rat.discrete_field [instance]
 
   definition divide (a b : rat) := algebra.divide a b
-  infix [priority rat.prio] `/` := divide
+  infix [priority rat.prio] / := divide
 
   definition pow (a : ℚ) (n : ℕ) : ℚ := algebra.pow a n
   infix [priority rat.prio] ^ := pow
   definition nmul (n : ℕ) (a : ℚ) : ℚ := algebra.nmul n a
-  infix [priority rat.prio] `⬝` := nmul
+  infix [priority rat.prio] ⬝ := nmul
   definition imul (i : ℤ) (a : ℚ) : ℚ := algebra.imul i a
 
   migrate from algebra with rat
diff --git a/library/data/real/basic.lean b/library/data/real/basic.lean
index da036dc7c..c232fa882 100644
--- a/library/data/real/basic.lean
+++ b/library/data/real/basic.lean
@@ -936,16 +936,16 @@ definition requiv.trans (s t u : reg_seq) (H : requiv s t) (H2 : requiv t u) : r
 definition radd (s t : reg_seq) : reg_seq :=
   reg_seq.mk (sadd (reg_seq.sq s) (reg_seq.sq t))
              (reg_add_reg (reg_seq.is_reg s) (reg_seq.is_reg t))
-infix `+` := radd
+infix + := radd
 
 definition rmul (s t : reg_seq) : reg_seq :=
   reg_seq.mk (smul (reg_seq.sq s) (reg_seq.sq t))
              (reg_mul_reg (reg_seq.is_reg s) (reg_seq.is_reg t))
-infix `*` := rmul
+infix * := rmul
 
 definition rneg (s : reg_seq) : reg_seq :=
   reg_seq.mk (sneg (reg_seq.sq s)) (reg_neg_reg (reg_seq.is_reg s))
-prefix `-` := rneg
+prefix - := rneg
 
 definition radd_well_defined {s t u v : reg_seq} (H : requiv s u) (H2 : requiv t v) :
            requiv (s + t) (u + v) :=
@@ -1025,13 +1025,13 @@ definition add (x y : ℝ) : ℝ :=
                      (take a b c d : reg_seq, take Hab : requiv a c, take Hcd : requiv b d,
                        quot.sound (radd_well_defined Hab Hcd)))
 protected definition prio := num.pred rat.prio
-infix [priority real.prio] `+` := add
+infix [priority real.prio] + := add
 
 definition mul (x y : ℝ) : ℝ :=
   (quot.lift_on₂ x y (λ a b, quot.mk (a * b))
                      (take a b c d : reg_seq, take Hab : requiv a c, take Hcd : requiv b d,
                        quot.sound (rmul_well_defined Hab Hcd)))
-infix [priority real.prio] `*` := mul
+infix [priority real.prio] * := mul
 
 definition neg (x : ℝ) : ℝ :=
   (quot.lift_on x (λ a, quot.mk (-a)) (take a b : reg_seq, take Hab : requiv a b,
diff --git a/library/data/set/basic.lean b/library/data/set/basic.lean
index ef9ab19f0..5edee0594 100644
--- a/library/data/set/basic.lean
+++ b/library/data/set/basic.lean
@@ -15,17 +15,17 @@ variable {X : Type}
 /- membership and subset -/
 
 definition mem [reducible] (x : X) (a : set X) := a x
-infix `∈` := mem
+infix ∈ := mem
 notation a ∉ b := ¬ mem a b
 
 theorem ext {a b : set X} (H : ∀x, x ∈ a ↔ x ∈ b) : a = b :=
 funext (take x, propext (H x))
 
 definition subset (a b : set X) := ∀⦃x⦄, x ∈ a → x ∈ b
-infix `⊆` := subset
+infix ⊆ := subset
 
 definition superset [reducible] (s t : set X) : Prop := t ⊆ s
-infix `⊇` := superset
+infix ⊇ := superset
 
 theorem subset.refl (a : set X) : a ⊆ a := take x, assume H, H
 
@@ -45,7 +45,7 @@ assume h₁ h₂, h₁ _ h₂
 /- strict subset -/
 
 definition strict_subset (a b : set X) := a ⊆ b ∧ a ≠ b
-infix `⊂`:50 := strict_subset
+infix ` ⊂ `:50 := strict_subset
 
 theorem strict_subset.irrefl (a : set X) : ¬ a ⊂ a :=
 assume h, absurd rfl (and.elim_right h)
@@ -235,18 +235,18 @@ ext (take x, !or.right_distrib)
 
 -- {x : X | P}
 definition set_of [reducible] (P : X → Prop) : set X := P
-notation `{` binder `|` r:(scoped:1 P, set_of P) `}` := r
+notation `{` binder ` | ` r:(scoped:1 P, set_of P) `}` := r
 
 -- {x ∈ s | P}
 definition sep (P : X → Prop) (s : set X) : set X := λx, x ∈ s ∧ P x
-notation `{` binder ∈ s `|` r:(scoped:1 p, sep p s) `}` := r
+notation `{` binder ` ∈ ` s ` | ` r:(scoped:1 p, sep p s) `}` := r
 
 /- insert -/
 
 definition insert (x : X) (a : set X) : set X := {y : X | y = x ∨ y ∈ a}
 
 -- '{x, y, z}
-notation `'{`:max a:(foldr `,` (x b, insert x b) ∅) `}`:0 := a
+notation `'{`:max a:(foldr `, ` (x b, insert x b) ∅) `}`:0 := a
 
 theorem subset_insert (x : X) (a : set X) : a ⊆ insert x a :=
 take y, assume ys, or.inr ys
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 570d428d3..37735ecd1 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -13,8 +13,8 @@ notation A ⊎ B := sum A B
 namespace sum
   notation A + B := sum A B
   namespace low_precedence_plus
-    reserve infixr `+`:25  -- conflicts with notation for addition
-    infixr `+` := sum
+    reserve infixr ` + `:25  -- conflicts with notation for addition
+    infixr + := sum
   end low_precedence_plus
 
   variables {A B : Type}
diff --git a/library/init/logic.lean b/library/init/logic.lean
index d52f34bbe..c21169480 100644
--- a/library/init/logic.lean
+++ b/library/init/logic.lean
@@ -152,7 +152,7 @@ section
   ne_false_of_self trivial
 end
 
-infixl `==`:50 := heq
+infixl ` == `:50 := heq
 
 namespace heq
   universe variable u
@@ -233,7 +233,7 @@ and.rec H₂ H₁
 
 /- or -/
 
-notation a `\/` b := or a b
+notation a \/ b := or a b
 notation a ∨ b := or a b
 
 namespace or
@@ -321,8 +321,8 @@ intro : ∀ (a : A), P a → Exists P
 
 definition exists.intro := @Exists.intro
 
-notation `exists` binders `,` r:(scoped P, Exists P) := r
-notation `∃` binders `,` r:(scoped P, Exists P) := r
+notation `exists` binders `, ` r:(scoped P, Exists P) := r
+notation `∃` binders `, ` r:(scoped P, Exists P) := r
 
 theorem exists.elim {A : Type} {p : A → Prop} {B : Prop}
   (H1 : ∃x, p x) (H2 : ∀ (a : A), p a → B) : B :=
diff --git a/library/init/nat.lean b/library/init/nat.lean
index 8ac028be3..584d251ad 100644
--- a/library/init/nat.lean
+++ b/library/init/nat.lean
@@ -16,15 +16,15 @@ namespace nat
   | refl : le a a
   | step : Π {b}, le a b → le a (succ b)
 
-  infix `≤` := le
+  infix ≤ := le
   attribute le.refl [refl]
 
   definition lt [reducible] (n m : ℕ) := succ n ≤ m
   definition ge [reducible] (n m : ℕ) := m ≤ n
   definition gt [reducible] (n m : ℕ) := succ m ≤ n
-  infix `<` := lt
-  infix `≥` := ge
-  infix `>` := gt
+  infix < := lt
+  infix ≥ := ge
+  infix > := gt
 
   definition pred [unfold 1] (a : nat) : nat :=
   nat.cases_on a zero (λ a₁, a₁)
diff --git a/library/init/prod.lean b/library/init/prod.lean
index 363df5b5c..275505d16 100644
--- a/library/init/prod.lean
+++ b/library/init/prod.lean
@@ -9,7 +9,7 @@ import init.num init.wf
 definition pair [constructor] := @prod.mk
 notation A × B := prod A B
 -- notation for n-ary tuples
-notation `(` h `,` t:(foldl `,` (e r, prod.mk r e) h) `)` := t
+notation `(` h `, ` t:(foldl `, ` (e r, prod.mk r e) h) `)` := t
 
 namespace prod
   notation [parsing-only] A * B := prod A B
diff --git a/library/init/reserved_notation.lean b/library/init/reserved_notation.lean
index 6af3efffa..62f698afc 100644
--- a/library/init/reserved_notation.lean
+++ b/library/init/reserved_notation.lean
@@ -33,65 +33,65 @@ num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (num.succ (
 /- Logical operations and relations -/
 
 reserve prefix `¬`:40
-reserve prefix `~`:40
-reserve infixr `∧`:35
-reserve infixr `/\`:35
-reserve infixr `\/`:30
-reserve infixr `∨`:30
-reserve infix `<->`:20
-reserve infix `↔`:20
-reserve infix `=`:50
-reserve infix `≠`:50
-reserve infix `≈`:50
-reserve infix `~`:50
-reserve infix `≡`:50
+reserve prefix ` ~ `:40
+reserve infixr ` ∧ `:35
+reserve infixr ` /\ `:35
+reserve infixr ` \/ `:30
+reserve infixr ` ∨ `:30
+reserve infix ` <-> `:20
+reserve infix ` ↔ `:20
+reserve infix ` = `:50
+reserve infix ` ≠ `:50
+reserve infix ` ≈ `:50
+reserve infix ` ~ `:50
+reserve infix ` ≡ `:50
 
-reserve infixr `∘`:60                   -- input with \comp
+reserve infixr ` ∘ `:60                 -- input with \comp
 reserve postfix `⁻¹`:std.prec.max_plus  -- input with \sy or \-1 or \inv
 
-reserve infixl `⬝`:75
-reserve infixr `▸`:75
-reserve infixr `▹`:75
+reserve infixl ` ⬝ `:75
+reserve infixr ` ▸ `:75
+reserve infixr ` ▹ `:75
 
 /- types and type constructors -/
 
-reserve infixl `⊎`:25
-reserve infixl `×`:30
+reserve infixl ` ⊎ `:25
+reserve infixl ` × `:30
 
 /- arithmetic operations -/
 
-reserve infixl `+`:65
-reserve infixl `-`:65
-reserve infixl `*`:70
-reserve infixl `div`:70
-reserve infixl `mod`:70
-reserve infixl `/`:70
+reserve infixl ` + `:65
+reserve infixl ` - `:65
+reserve infixl ` * `:70
+reserve infixl ` div `:70
+reserve infixl ` mod `:70
+reserve infixl ` / `:70
 reserve prefix `-`:100
-reserve infix `^`:80
+reserve infix ` ^ `:80
 
-reserve infix `<=`:50
-reserve infix `≤`:50
-reserve infix `<`:50
-reserve infix `>=`:50
-reserve infix `≥`:50
-reserve infix `>`:50
+reserve infix ` <= `:50
+reserve infix ` ≤ `:50
+reserve infix ` < `:50
+reserve infix ` >= `:50
+reserve infix ` ≥ `:50
+reserve infix ` > `:50
 
 /- boolean operations -/
 
-reserve infixl `&&`:70
-reserve infixl `||`:65
+reserve infixl ` && `:70
+reserve infixl ` || `:65
 
 /- set operations -/
 
-reserve infix `∈`:50
-reserve infix `∉`:50
-reserve infixl `∩`:70
-reserve infixl `∪`:65
-reserve infix `⊆`:50
-reserve infix `⊇`:50
+reserve infix ` ∈ `:50
+reserve infix ` ∉ `:50
+reserve infixl ` ∩ `:70
+reserve infixl ` ∪ `:65
+reserve infix ` ⊆ `:50
+reserve infix ` ⊇ `:50
 
 /- other symbols -/
 
-reserve infix `∣`:50
-reserve infixl `++`:65
-reserve infixr `::`:65
+reserve infix ` ∣ `:50
+reserve infixl ` ++ `:65
+reserve infixr ` :: `:65
diff --git a/library/init/sigma.lean b/library/init/sigma.lean
index 975cebfb3..efc7dbd91 100644
--- a/library/init/sigma.lean
+++ b/library/init/sigma.lean
@@ -7,9 +7,9 @@ prelude
 import init.datatypes init.num init.wf init.logic init.tactic
 
 definition dpair := @sigma.mk
-notation `Σ` binders `,` r:(scoped P, sigma P) := r
+notation `Σ` binders `, ` r:(scoped P, sigma P) := r
 -- notation for n-ary tuples; input ⟨ ⟩ as \< \>
-notation `⟨`:max t:(foldr `,` (e r, sigma.mk e r)) `⟩`:0 := t
+notation `⟨`:max t:(foldr `, ` (e r, sigma.mk e r)) `⟩`:0 := t
 
 lemma ex_of_sig {A : Type} {P : A → Prop} : (Σ x, P x) → ∃ x, P x :=
 assume h, obtain x hx, from h, exists.intro x hx
diff --git a/library/init/subtype.lean b/library/init/subtype.lean
index 7018cd543..713359c54 100644
--- a/library/init/subtype.lean
+++ b/library/init/subtype.lean
@@ -12,7 +12,7 @@ set_option structure.proj_mk_thm true
 structure subtype {A : Type} (P : A → Prop) :=
 tag :: (elt_of : A) (has_property : P elt_of)
 
-notation `{` binder `|` r:(scoped:1 P, subtype P) `}` := r
+notation `{` binder ` | ` r:(scoped:1 P, subtype P) `}` := r
 
 definition ex_of_sub {A : Type} {P : A → Prop} : { x | P x } → ∃ x, P x
 | (subtype.tag a h) := exists.intro a h