diff --git a/library/standard/bool.lean b/library/standard/bool.lean
index 008bc7588..12ea0188f 100644
--- a/library/standard/bool.lean
+++ b/library/standard/bool.lean
@@ -21,7 +21,7 @@ definition cond {A : Type} (b : bool) (t e : A)
 := bool_rec e t b
 
 theorem dichotomy (b : bool) : b = '0 ∨ b = '1
-:= induction_on b (or_intro_left _ (refl '0)) (or_intro_right _ (refl '1))
+:= induction_on b (or_inl (refl '0)) (or_inr (refl '1))
 
 theorem cond_b0 {A : Type} (t e : A) : cond '0 t e = e
 := refl (cond '0 t e)
@@ -79,8 +79,8 @@ theorem bor_to_or {a b : bool} : a || b = '1 → a = '1 ∨ b = '1
 := bool_rec
     (assume H : '0 || b = '1,
      have Hb : b = '1, from (bor_b0_left b) ▸ H,
-     or_intro_right _ Hb)
-    (assume H, or_intro_left _ (refl '1))
+     or_inr Hb)
+    (assume H, or_inl (refl '1))
     a
 
 definition band (a b : bool)
diff --git a/library/standard/classical.lean b/library/standard/classical.lean
index 271fa6bb4..c4e112410 100644
--- a/library/standard/classical.lean
+++ b/library/standard/classical.lean
@@ -13,13 +13,13 @@ theorem case (P : Prop → Prop) (H1 : P true) (H2 : P false) (a : Prop) : P a
 
 theorem em (a : Prop) : a ∨ ¬a
 := or_elim (prop_complete a)
-     (assume Ht : a = true,  or_intro_left (¬a) (eqt_elim Ht))
-     (assume Hf : a = false, or_intro_right a (eqf_elim Hf))
+     (assume Ht : a = true,  or_inl (eqt_elim Ht))
+     (assume Hf : a = false, or_inr (eqf_elim Hf))
 
 theorem prop_complete_swapped (a : Prop) : a = false ∨ a = true
 := case (λ x, x = false ∨ x = true)
-        (or_intro_right (true = false) (refl true))
-        (or_intro_left  (false = true) (refl false))
+        (or_inr (refl true))
+        (or_inl (refl false))
         a
 
 theorem not_true : (¬true) = false
@@ -86,9 +86,9 @@ theorem heq_id {A : Type} (a : A) : (a == a) = true
 theorem not_or (a b : Prop) : (¬(a ∨ b)) = (¬a ∧ ¬b)
 := propext
      (assume H, or_elim (em a)
-       (assume Ha, absurd_elim (¬a ∧ ¬b) (or_intro_left b Ha) H)
+       (assume Ha, absurd_elim (¬a ∧ ¬b) (or_inl Ha) H)
        (assume Hna, or_elim (em b)
-         (assume Hb, absurd_elim (¬a ∧ ¬b) (or_intro_right a Hb) H)
+         (assume Hb, absurd_elim (¬a ∧ ¬b) (or_inr Hb) H)
          (assume Hnb, and_intro Hna Hnb)))
      (assume (H : ¬a ∧ ¬b) (N : a ∨ b),
        or_elim N
@@ -100,8 +100,8 @@ theorem not_and (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b)
      (assume H, or_elim (em a)
        (assume Ha, or_elim (em b)
        (assume Hb, absurd_elim (¬a ∨ ¬b) (and_intro Ha Hb) H)
-         (assume Hnb, or_intro_right (¬a) Hnb))
-         (assume Hna, or_intro_left (¬b) Hna))
+         (assume Hnb, or_inr Hnb))
+         (assume Hna, or_inl Hna))
      (assume (H : ¬a ∨ ¬b) (N : a ∧ b),
        or_elim H
          (assume Hna, absurd (and_elim_left N) Hna)
@@ -110,8 +110,8 @@ theorem not_and (a b : Prop) : (¬(a ∧ b)) = (¬a ∨ ¬b)
 theorem imp_or (a b : Prop) : (a → b) = (¬a ∨ b)
 := propext
      (assume H : a → b, (or_elim (em a)
-       (assume Ha  : a,   or_intro_right (¬a) (H Ha))
-       (assume Hna : ¬a, or_intro_left b Hna)))
+       (assume Ha  : a,   or_inr (H Ha))
+       (assume Hna : ¬a, or_inl Hna)))
      (assume (H : ¬a ∨ b) (Ha : a),
        resolve_right H ((not_not_eq a)⁻¹ ◂ Ha))
 
diff --git a/library/standard/decidable.lean b/library/standard/decidable.lean
index 56978cbeb..3546956ab 100644
--- a/library/standard/decidable.lean
+++ b/library/standard/decidable.lean
@@ -12,7 +12,7 @@ theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2
 := decidable_rec H1 H2 H
 
 theorem em (p : Prop) (H : decidable p) : p ∨ ¬p
-:= induction_on H (λ Hp, or_intro_left _ Hp) (λ Hnp, or_intro_right _ Hnp)
+:= induction_on H (λ Hp, or_inl Hp) (λ Hnp, or_inr Hnp)
 
 definition rec_on [inline] {p : Prop} {C : Type} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C
 := decidable_rec H1 H2 H
@@ -44,9 +44,9 @@ theorem decidable_and [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable
 
 theorem decidable_or [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) : decidable (a ∨ b)
 := rec_on Ha
-    (assume Ha  : a, inl (or_intro_left b Ha))
+    (assume Ha  : a, inl (or_inl Ha))
     (assume Hna : ¬a, rec_on Hb
-      (assume Hb  : b,  inl (or_intro_right a Hb))
+      (assume Hb  : b,  inl (or_inr Hb))
       (assume Hnb : ¬b, inr (or_not_intro Hna Hnb)))
 
 theorem decidable_not [instance] {a : Prop} (Ha : decidable a) : decidable (¬a)
diff --git a/library/standard/diaconescu.lean b/library/standard/diaconescu.lean
index 5d338a18f..93918f3cc 100644
--- a/library/standard/diaconescu.lean
+++ b/library/standard/diaconescu.lean
@@ -17,28 +17,28 @@ definition u [private] := epsilon (λ x, x = true ∨ p)
 definition v [private] := epsilon (λ x, x = false ∨ p)
 
 lemma u_def [private] : u = true ∨ p
-:= epsilon_ax (exists_intro true (or_intro_left p (refl true)))
+:= epsilon_ax (exists_intro true (or_inl (refl true)))
 
 lemma v_def [private] : v = false ∨ p
-:= epsilon_ax (exists_intro false (or_intro_left p (refl false)))
+:= epsilon_ax (exists_intro false (or_inl (refl false)))
 
 lemma uv_implies_p [private] : ¬(u = v) ∨ p
 := or_elim u_def
     (assume Hut : u = true, or_elim v_def
       (assume Hvf : v = false,
         have Hne : ¬(u = v), from Hvf⁻¹ ▸ Hut⁻¹ ▸ true_ne_false,
-        or_intro_left p Hne)
-      (assume Hp : p, or_intro_right (¬u = v) Hp))
-    (assume Hp : p, or_intro_right (¬u = v) Hp)
+        or_inl Hne)
+      (assume Hp : p, or_inr Hp))
+    (assume Hp : p, or_inr Hp)
 
 lemma p_implies_uv [private] : p → u = v
 := assume Hp : p,
    have Hpred : (λ x, x = true ∨ p) = (λ x, x = false ∨ p), from
      funext (take x : Prop,
        have Hl : (x = true ∨ p) → (x = false ∨ p), from
-         assume A, or_intro_right (x = false) Hp,
+         assume A, or_inr Hp,
        have Hr : (x = false ∨ p) → (x = true ∨ p), from
-         assume A, or_intro_right (x = true) Hp,
+         assume A, or_inr Hp,
        show (x = true ∨ p) = (x = false ∨ p), from
          propext Hl Hr),
    show u = v, from
@@ -47,6 +47,6 @@ lemma p_implies_uv [private] : p → u = v
 theorem em : p ∨ ¬p
 := have H : ¬(u = v) → ¬p, from contrapos p_implies_uv,
    or_elim uv_implies_p
-     (assume Hne : ¬(u = v), or_intro_right p (H Hne))
-     (assume Hp : p, or_intro_left (¬p) Hp)
+     (assume Hne : ¬(u = v), or_inr (H Hne))
+     (assume Hp : p, or_inl Hp)
 end
diff --git a/library/standard/logic.lean b/library/standard/logic.lean
index 0bcd5c090..8bbd674dd 100644
--- a/library/standard/logic.lean
+++ b/library/standard/logic.lean
@@ -81,6 +81,9 @@ inductive or (a b : Prop) : Prop :=
 infixr `\/`:30 := or
 infixr `∨`:30 := or
 
+theorem or_inl {a b : Prop} (Ha : a) : a ∨ b := or_intro_left b Ha
+theorem or_inr {a b : Prop} (Hb : b) : a ∨ b := or_intro_right a Hb
+
 theorem or_elim {a b c : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → c) : c
 := or_rec H2 H3 H1
 
@@ -91,7 +94,7 @@ theorem resolve_left {a b : Prop} (H1 : a ∨ b) (H2 : ¬b) : a
 := or_elim H1 (assume Ha, Ha) (assume Hb, absurd_elim a Hb H2)
 
 theorem or_swap {a b : Prop} (H : a ∨ b) : b ∨ a
-:= or_elim H (assume Ha, or_intro_right b Ha) (assume Hb, or_intro_left a Hb)
+:= or_elim H (assume Ha, or_inr Ha) (assume Hb, or_inl Hb)
 
 theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b)
 := assume H : a ∨ b, or_elim H
@@ -100,18 +103,18 @@ theorem or_not_intro {a b : Prop} (Hna : ¬a) (Hnb : ¬b) : ¬(a ∨ b)
 
 theorem or_imp_or {a b c d : Prop} (H1 : a ∨ b) (H2 : a → c) (H3 : b → d) : c ∨ d
 := or_elim H1
-    (assume Ha : a, or_intro_left _ (H2 Ha))
-    (assume Hb : b, or_intro_right _ (H3 Hb))
+    (assume Ha : a, or_inl (H2 Ha))
+    (assume Hb : b, or_inr (H3 Hb))
 
 theorem imp_or_left {a b c : Prop} (H1 : a ∨ c) (H : a → b) : b ∨ c
 := or_elim H1
-    (assume H2 : a, or_intro_left _ (H H2))
-    (assume H2 : c, or_intro_right _ H2)
+    (assume H2 : a, or_inl (H H2))
+    (assume H2 : c, or_inr H2)
 
 theorem imp_or_right {a b c : Prop} (H1 : c ∨ a) (H : a → b) : c ∨ b
 := or_elim H1
-    (assume H2 : c, or_intro_left _ H2)
-    (assume H2 : a, or_intro_right _ (H H2))
+    (assume H2 : c, or_inl H2)
+    (assume H2 : a, or_inr (H H2))
 
 inductive eq {A : Type} (a : A) : A → Prop :=
 | refl : eq a a
@@ -271,14 +274,14 @@ theorem or_assoc (a b c : Prop) : (a ∨ b) ∨ c ↔ a ∨ (b ∨ c)
 := iff_intro
     (assume H, or_elim H
       (assume H1, or_elim H1
-        (assume Ha, or_intro_left _ Ha)
-        (assume Hb, or_intro_right a (or_intro_left c Hb)))
-      (assume Hc, or_intro_right a (or_intro_right b Hc)))
+        (assume Ha, or_inl Ha)
+        (assume Hb, or_inr (or_inl Hb)))
+      (assume Hc, or_inr (or_inr Hc)))
     (assume H, or_elim H
-      (assume Ha, (or_intro_left c (or_intro_left b Ha)))
+      (assume Ha, (or_inl (or_inl Ha)))
       (assume H1, or_elim H1
-        (assume Hb, or_intro_left c (or_intro_right a Hb))
-        (assume Hc, or_intro_right _ Hc)))
+        (assume Hb, or_inl (or_inr Hb))
+        (assume Hc, or_inr Hc)))
 
 inductive Exists {A : Type} (P : A → Prop) : Prop :=
 | exists_intro : ∀ (a : A), P a → Exists P
diff --git a/library/standard/nat.lean b/library/standard/nat.lean
index 36b35f568..c6fcd3df2 100644
--- a/library/standard/nat.lean
+++ b/library/standard/nat.lean
@@ -55,8 +55,8 @@ theorem pred_succ (n : ℕ) : pred (succ n) = n
 
 theorem zero_or_succ (n : ℕ) : n = 0 ∨ n = succ (pred n)
 := induction_on n
-    (or_intro_left _ (refl 0))
-    (take m IH, or_intro_right _
+    (or_inl (refl 0))
+    (take m IH, or_inr
       (show succ m = succ (pred (succ m)), from congr2 succ (pred_succ m⁻¹)))
 
 theorem zero_or_succ2 (n : ℕ) : n = 0 ∨ ∃k, n = succ k
@@ -366,11 +366,11 @@ theorem mul_one_left (n : ℕ) : 1 * n = n
 theorem mul_eq_zero {n m : ℕ} (H : n * m = 0) : n = 0 ∨ m = 0
 :=
   discriminate
-    (take Hn : n = 0, or_intro_left _ Hn)
+    (take Hn : n = 0, or_inl Hn)
     (take (k : ℕ),
       assume (Hk : n = succ k),
       discriminate
-        (take (Hm : m = 0), or_intro_right _ Hm)
+        (take (Hm : m = 0), or_inr Hm)
         (take (l : ℕ),
           assume (Hl : m = succ l),
           have Heq : succ (k * succ l + l) = n * m, from
@@ -495,7 +495,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
           n = n + 0 : (add_zero_right n)⁻¹
             ... = n + k : {H3⁻¹}
             ... = m : Hk,
-      or_intro_right _ Heq)
+      or_inr Heq)
     (take l:ℕ,
       assume H3 : k = succ l,
       have Hlt : succ n ≤ m, from
@@ -504,7 +504,7 @@ theorem succ_le_left_or {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
             succ n + l = n + succ l : add_move_succ n l
               ... = n + k : {H3⁻¹}
               ... = m : Hk)),
-      or_intro_left _ Hlt)
+      or_inl Hlt)
 
 theorem succ_le_left {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m
 := resolve_left (succ_le_left_or H1) H2
@@ -556,7 +556,7 @@ theorem pred_le {n m : ℕ} (H : n ≤ m) : pred n ≤ pred m
 theorem pred_le_left_inv {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = succ m
 := discriminate
     (take Hn : n = 0,
-      or_intro_left _ (subst (symm Hn) (zero_le m)))
+      or_inl (subst (symm Hn) (zero_le m)))
     (take k : ℕ,
       assume Hn : n = succ k,
       have H2 : pred n = k,
@@ -582,7 +582,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
           n = n + 0 : symm (add_zero_right n)
             ... = n + k : {symm H3}
             ... = m : Hk,
-      or_intro_right _ Heq)
+      or_inr Heq)
     (take l : nat,
       assume H3 : k = succ l,
       have Hlt : succ n ≤ m, from
@@ -591,7 +591,7 @@ theorem le_imp_succ_le_or_eq {n m : ℕ} (H : n ≤ m) : succ n ≤ m ∨ n = m
             succ n + l = n + succ l : add_move_succ n l
               ... = n + k : {symm H3}
               ... = m : Hk)),
-      or_intro_left _ Hlt)
+      or_inl Hlt)
 
 theorem le_ne_imp_succ_le {n m : ℕ} (H1 : n ≤ m) (H2 : n ≠ m) : succ n ≤ m
 := resolve_left (le_imp_succ_le_or_eq H1) H2
@@ -619,7 +619,7 @@ theorem pred_le_imp_le_or_eq {n m : ℕ} (H : pred n ≤ m) : n ≤ m ∨ n = su
 :=
   discriminate
     (take Hn : n = 0,
-      or_intro_left _ (subst (symm Hn) (zero_le m)))
+      or_inl (subst (symm Hn) (zero_le m)))
     (take k : nat,
       assume Hn : n = succ k,
       have H2 : pred n = k,
@@ -789,7 +789,7 @@ theorem succ_lt_right {n m : ℕ} (H : n < m) : n < succ m
 
 theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
 := induction_on n
-    (or_intro_left _ (zero_le m))
+    (or_inl (zero_le m))
     (take (k : ℕ),
       assume IH : k ≤ m ∨ m < k,
       or_elim IH
@@ -803,7 +803,7 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
                     ... = k + 0 : {H2}
                     ... = k : add_zero_right k,
               have H4 : m < succ k, from subst  H3 (lt_self_succ m),
-              or_intro_right _ H4)
+              or_inr H4)
             (take l2 : ℕ,
               assume H2 : l = succ l2,
               have H3 : succ k + l2 = m,
@@ -811,8 +811,8 @@ theorem le_or_lt (n m : ℕ) : n ≤ m ∨ m < n
                   succ k + l2 = k + succ l2 : add_move_succ k l2
                     ... = k + l : {symm H2}
                     ... = m : Hl,
-              or_intro_left _ (le_intro H3)))
-        (assume H : m < k, or_intro_right _ (succ_lt_right H)))
+              or_inl (le_intro H3)))
+        (assume H : m < k, or_inr (succ_lt_right H)))
 
 theorem trichotomy_alt (n m : ℕ) : (n < m ∨ n = m) ∨ m < n
 := or_imp_or (le_or_lt n m) (assume H : n ≤ m, le_imp_lt_or_eq H) (assume H : m < n, H)