diff --git a/library/data/bool.lean b/library/data/bool.lean
index 4a5da82158..266fbb753d 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -138,7 +138,7 @@ namespace bool
   protected theorem is_inhabited [instance] : inhabited bool :=
   inhabited.mk ff
 
-  protected theorem has_decidable_eq [instance] : decidable_eq bool :=
+  protected definition has_decidable_eq [instance] : decidable_eq bool :=
   take a b : bool,
     rec_on a
       (rec_on b (inl rfl) (inr ff_ne_tt))
diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index c17fe1adfe..0bc3946fbc 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -203,8 +203,9 @@ exists_intro (pr1 (rep a))
       a = psub (rep a) : (psub_rep a)⁻¹
     ... = psub (pair (pr1 (rep a)) (pr2 (rep a))) : {(prod_ext (rep a))⁻¹}))
 
-protected theorem has_decidable_eq [instance] : decidable_eq ℤ :=
-take a b : ℤ, _
+-- TODO it should not be opaque.
+protected opaque definition has_decidable_eq [instance] : decidable_eq ℤ :=
+_
 
 irreducible int
 definition of_nat [coercion] (n : ℕ) : ℤ := psub (pair n 0)
diff --git a/library/data/int/order.lean b/library/data/int/order.lean
index 314bb4892a..87b904c956 100644
--- a/library/data/int/order.lean
+++ b/library/data/int/order.lean
@@ -422,8 +422,8 @@ Hn⁻¹ ▸ congr_arg of_nat (to_nat_of_nat n)
 theorem of_nat_nonneg (n : ℕ) : of_nat n ≥ 0 :=
 iff.mp (iff.symm (le_of_nat _ _)) zero_le
 
-theorem le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
-have aux : ∀x, decidable (0 ≤ x), from
+definition le_decidable [instance] {a b : ℤ} : decidable (a ≤ b) :=
+have aux : Πx, decidable (0 ≤ x), from
   take x,
     have H : 0 ≤ x ↔ of_nat (to_nat x) = x, from
       iff.intro
@@ -432,9 +432,9 @@ have aux : ∀x, decidable (0 ≤ x), from
     decidable_iff_equiv _ (iff.symm H),
 decidable_iff_equiv (aux _) (iff.symm (le_iff_sub_nonneg a b))
 
-theorem ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b)
-theorem lt_decidable [instance] {a b : ℤ} : decidable (a < b)
-theorem gt_decidable [instance] {a b : ℤ} : decidable (a > b)
+definition ge_decidable [instance] {a b : ℤ} : decidable (a ≥ b) := _
+definition lt_decidable [instance] {a b : ℤ} : decidable (a < b) := _
+definition gt_decidable [instance] {a b : ℤ} : decidable (a > b) := _
 
 --to_nat_neg is already taken... rename?
 theorem to_nat_negative {a : ℤ} (H : a ≤ 0) : (to_nat a) = -a :=
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index 0ebc0b79f7..6192a1eba3 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -204,7 +204,7 @@ induction_on l
           from H3 ▸ rfl,
         exists_intro _ (exists_intro _ H4)))
 
-theorem mem_is_decidable [instance] {H : decidable_eq T} {x : T} {l : list T} : decidable (x ∈ l) :=
+definition mem_is_decidable [instance] {H : decidable_eq T} {x : T} {l : list T} : decidable (x ∈ l) :=
 rec_on l
   (decidable.inr (iff.false_elim mem_nil))
   (λ (h : T) (l : list T) (iH : decidable (x ∈ l)),
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index b38018af49..07c962ff3d 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -105,7 +105,7 @@ induction_on n
     absurd H ne)
   (take k IH H, IH (succ_inj H))
 
-protected theorem has_decidable_eq [instance] : decidable_eq ℕ :=
+protected definition has_decidable_eq [instance] : decidable_eq ℕ :=
 take n m : ℕ,
 have general : ∀n, decidable (n = m), from
   rec_on m
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index f700863d3c..79bc63786c 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -230,7 +230,7 @@ le_trans (mul_le_right H1 m) (mul_le_left H2 k)
 
 -- mul_le_[left|right]_inv below
 
-theorem le_decidable [instance] (n m : ℕ) : decidable (n ≤ m) :=
+definition le_decidable [instance] (n m : ℕ) : decidable (n ≤ m) :=
 have general : ∀n, decidable (n ≤ m), from
   rec_on m
     (take n,
@@ -422,9 +422,9 @@ theorem not_le_imp_gt {n m : ℕ} (H : ¬ n ≤ m) : n > m :=
 or.resolve_right le_or_gt H
 
 -- The following three theorems are automatically proved using the instance le_decidable
-theorem lt_decidable [instance] (n m : ℕ) : decidable (n < m)
-theorem gt_decidable [instance] (n m : ℕ) : decidable (n > m)
-theorem ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m)
+definition lt_decidable [instance] (n m : ℕ) : decidable (n < m) := _
+definition gt_decidable [instance] (n m : ℕ) : decidable (n > m) := _
+definition ge_decidable [instance] (n m : ℕ) : decidable (n ≥ m) := _
 
 -- Note: interaction with multiplication under "positivity"
 
diff --git a/library/data/option.lean b/library/data/option.lean
index 5857b7459b..387a499139 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -38,7 +38,7 @@ namespace option
   protected theorem is_inhabited [instance] (A : Type) : inhabited (option A) :=
   inhabited.mk none
 
-  protected theorem has_decidable_eq [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) :=
+  protected definition has_decidable_eq [instance] {A : Type} (H : decidable_eq A) : decidable_eq (option A) :=
   take o₁ o₂ : option A,
     rec_on o₁
       (rec_on o₂ (inl rfl) (take a₂, (inr (none_ne_some a₂))))
diff --git a/library/data/prod.lean b/library/data/prod.lean
index d8d41cd9dd..e12b3e4aee 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -48,7 +48,7 @@ section
   protected theorem is_inhabited [instance] (H1 : inhabited A) (H2 : inhabited B) : inhabited (prod A B) :=
   inhabited.destruct H1 (λa, inhabited.destruct H2 (λb, inhabited.mk (pair a b)))
 
-  protected theorem has_decidable_eq [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) :=
+  protected definition has_decidable_eq [instance] (H1 : decidable_eq A) (H2 : decidable_eq B) : decidable_eq (A × B) :=
   take u v : A × B,
     have H3 : u = v ↔ (pr1 u = pr1 v) ∧ (pr2 u = pr2 v), from
       iff.intro
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index c462e789b3..3e217a162d 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -41,7 +41,7 @@ section
   protected theorem is_inhabited [instance] {a : A} (H : P a) : inhabited {x, P x} :=
   inhabited.mk (tag a H)
 
-  protected theorem has_decidable_eq [instance] (H : decidable_eq A) : decidable_eq {x, P x} :=
+  protected definition has_decidable_eq [instance] (H : decidable_eq A) : decidable_eq {x, P x} :=
   take a1 a2 : {x, P x},
     have H1 : (a1 = a2) ↔ (elt_of a1 = elt_of a2), from
       iff.intro (assume H, eq.subst H rfl) (assume H, equal H),
diff --git a/library/data/sum.lean b/library/data/sum.lean
index 9db6904a1b..f517f66a8a 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -55,7 +55,7 @@ namespace sum
   protected theorem is_inhabited_right [instance] {A B : Type} (H : inhabited B) : inhabited (A ⊎ B) :=
   inhabited.mk (inr A (default B))
 
-  protected theorem has_eq_decidable [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) :
+  protected definition has_eq_decidable [instance] {A B : Type} (H1 : decidable_eq A) (H2 : decidable_eq B) :
        decidable_eq (A ⊎ B) :=
   take s1 s2 : A ⊎ B,
     rec_on s1
diff --git a/library/data/unit.lean b/library/data/unit.lean
index 36a1289a89..aee94ce84c 100644
--- a/library/data/unit.lean
+++ b/library/data/unit.lean
@@ -18,6 +18,6 @@ namespace unit
   protected theorem is_inhabited [instance] : inhabited unit :=
   inhabited.mk ⋆
 
-  protected theorem has_decidable_eq [instance] : decidable_eq unit :=
+  protected definition has_decidable_eq [instance] : decidable_eq unit :=
   take (a b : unit), inl (equal a b)
 end unit
diff --git a/library/logic/core/decidable.lean b/library/logic/core/decidable.lean
index 876ec1eba2..44c373e7bb 100644
--- a/library/logic/core/decidable.lean
+++ b/library/logic/core/decidable.lean
@@ -10,10 +10,10 @@ inr : ¬p → decidable p
 
 namespace decidable
 
-theorem true_decidable [instance] : decidable true :=
+definition true_decidable [instance] : decidable true :=
 inl trivial
 
-theorem false_decidable [instance] : decidable false :=
+definition false_decidable [instance] : decidable false :=
 inr not_false_trivial
 
 protected theorem induction_on {p : Prop} {C : Prop} (H : decidable p) (H1 : p → C) (H2 : ¬p → C) : C :=
@@ -38,7 +38,7 @@ decidable.rec
 theorem em (p : Prop) {H : decidable p} : p ∨ ¬p :=
 induction_on H (λ Hp, or.inl Hp) (λ Hnp, or.inr Hnp)
 
-theorem by_cases {a : Prop} {b : Type} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b :=
+definition by_cases {a : Prop} {b : Type} {C : decidable a} (Hab : a → b) (Hnab : ¬a → b) : b :=
 rec_on C (assume Ha, Hab Ha) (assume Hna, Hnab Hna)
 
 theorem by_contradiction {p : Prop} {Hp : decidable p} (H : ¬p → false) : p :=
@@ -46,7 +46,7 @@ or.elim (em p)
   (assume H1 : p, H1)
   (assume H1 : ¬p, false_elim (H H1))
 
-theorem and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+definition and_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a ∧ b) :=
 rec_on Ha
   (assume Ha  : a, rec_on Hb
@@ -54,7 +54,7 @@ rec_on Ha
     (assume Hnb : ¬b, inr (and.not_right a Hnb)))
   (assume Hna : ¬a, inr (and.not_left b Hna))
 
-theorem or_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+definition or_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a ∨ b) :=
 rec_on Ha
   (assume Ha  : a, inl (or.inl Ha))
@@ -62,12 +62,12 @@ rec_on Ha
     (assume Hb  : b,  inl (or.inr Hb))
     (assume Hnb : ¬b, inr (or.not_intro Hna Hnb)))
 
-theorem not_decidable [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) :=
+definition not_decidable [instance] {a : Prop} (Ha : decidable a) : decidable (¬a) :=
 rec_on Ha
   (assume Ha,  inr (not_not_intro Ha))
   (assume Hna, inl Hna)
 
-theorem iff_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+definition iff_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a ↔ b) :=
 rec_on Ha
   (assume Ha, rec_on Hb
@@ -78,7 +78,7 @@ rec_on Ha
     (assume Hnb : ¬b, inl
         (iff.intro (assume Ha, absurd Ha Hna) (assume Hb, absurd Hb Hnb))))
 
-theorem implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
+definition implies_decidable [instance] {a b : Prop} (Ha : decidable a) (Hb : decidable b) :
   decidable (a → b) :=
 rec_on Ha
   (assume Ha  : a, rec_on Hb
@@ -86,12 +86,12 @@ rec_on Ha
     (assume Hnb : ¬b, inr (assume H : a → b, absurd (H Ha) Hnb)))
   (assume Hna : ¬a, inl (assume Ha, absurd Ha Hna))
 
-theorem decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b :=
+definition decidable_iff_equiv {a b : Prop} (Ha : decidable a) (H : a ↔ b) : decidable b :=
 rec_on Ha
   (assume Ha : a,   inl (iff.elim_left H Ha))
   (assume Hna : ¬a, inr (iff.elim_left (iff.flip_sign H) Hna))
 
-theorem decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b :=
+definition decidable_eq_equiv {a b : Prop} (Ha : decidable a) (H : a = b) : decidable b :=
 decidable_iff_equiv Ha (eq_to_iff H)
 
 end decidable