From c4cc837e34a5d80f08e8687ea8417bf0ee255a99 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 21 Aug 2014 18:39:38 -0700
Subject: [PATCH] refactor(library/standard): define abbreviations using '@'

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
---
 library/standard/logic/connectives/basic.lean  | 10 +++++-----
 .../standard/logic/connectives/instances.lean  | 18 +++++++++---------
 2 files changed, 14 insertions(+), 14 deletions(-)

diff --git a/library/standard/logic/connectives/basic.lean b/library/standard/logic/connectives/basic.lean
index 3a8a30e22..0fd2ecf28 100644
--- a/library/standard/logic/connectives/basic.lean
+++ b/library/standard/logic/connectives/basic.lean
@@ -153,12 +153,12 @@ theorem iff_intro {a b : Prop} (H1 : a → b) (H2 : b → a) : a ↔ b := and_in
 
 theorem iff_elim {a b c : Prop} (H1 : (a → b) → (b → a) → c) (H2 : a ↔ b) : c := and_rec H1 H2
 
-theorem iff_elim_left ⦃a b : Prop⦄ (H : a ↔ b) : a → b :=
+theorem iff_elim_left {a b : Prop} (H : a ↔ b) : a → b :=
 iff_elim (assume H1 H2, H1) H
 
-abbreviation iff_mp := iff_elim_left
+abbreviation iff_mp := @iff_elim_left
 
-theorem iff_elim_right ⦃a b : Prop⦄ (H : a ↔ b) : b → a :=
+theorem iff_elim_right {a b : Prop} (H : a ↔ b) : b → a :=
 iff_elim (assume H1 H2, H2) H
 
 theorem iff_flip_sign {a b : Prop} (H1 : a ↔ b) : ¬a ↔ ¬b :=
@@ -169,12 +169,12 @@ iff_intro
 theorem iff_refl (a : Prop) : a ↔ a :=
 iff_intro (assume H, H) (assume H, H)
 
-theorem iff_trans ⦃a b c : Prop⦄ (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c :=
+theorem iff_trans {a b c : Prop} (H1 : a ↔ b) (H2 : b ↔ c) : a ↔ c :=
 iff_intro
   (assume Ha, iff_elim_left H2 (iff_elim_left H1 Ha))
   (assume Hc, iff_elim_right H1 (iff_elim_right H2 Hc))
 
-theorem iff_symm ⦃a b : Prop⦄ (H : a ↔ b) : b ↔ a :=
+theorem iff_symm {a b : Prop} (H : a ↔ b) : b ↔ a :=
 iff_intro
   (assume Hb, iff_elim_right H Hb)
   (assume Ha, iff_elim_left H Ha)
diff --git a/library/standard/logic/connectives/instances.lean b/library/standard/logic/connectives/instances.lean
index 79702797e..6101ed0ff 100644
--- a/library/standard/logic/connectives/instances.lean
+++ b/library/standard/logic/connectives/instances.lean
@@ -111,7 +111,7 @@ relation.mp_like_mk (iff_elim_left H)
 -- Substition for iff
 -- ------------------
 
-theorem subst_iff ⦃P : Prop → Prop⦄ {C : congr iff iff P} {a b : Prop} (H : a ↔ b) (H1 : P a) :
+theorem subst_iff {P : Prop → Prop} {C : congr iff iff P} {a b : Prop} (H : a ↔ b) (H1 : P a) :
   P b :=
 @general_operations.subst Prop iff P C a b H H1
 
@@ -124,14 +124,14 @@ calc_trans iff_trans
 calc_subst subst_iff
 
 namespace iff_ops
-  postfix `⁻¹`:100 := iff_symm
-  infixr `⬝`:75     := iff_trans
-  infixr `▸`:75    := subst_iff
-  abbreviation refl := iff_refl
-  abbreviation symm := iff_symm
-  abbreviation trans := iff_trans
-  abbreviation subst := subst_iff
-  abbreviation mp := iff_mp
+  postfix `⁻¹`:100   := iff_symm
+  infixr `⬝`:75      := iff_trans
+  infixr `▸`:75      := subst_iff
+  abbreviation refl  := iff_refl
+  abbreviation symm  := @iff_symm
+  abbreviation trans := @iff_trans
+  abbreviation subst := @subst_iff
+  abbreviation mp    := @iff_mp
 end iff_ops