From ff9a07500d93ebbd3fcf188c9634913903645b5d Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Tue, 9 Sep 2014 13:15:06 -0700
Subject: [PATCH] feat(library/data/int/basic): create alias for int.int

---
 library/data/int/basic.lean | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/library/data/int/basic.lean b/library/data/int/basic.lean
index a2d0630fe..4dd940352 100644
--- a/library/data/int/basic.lean
+++ b/library/data/int/basic.lean
@@ -184,7 +184,7 @@ representative_map_idempotent_equiv proj_rel @proj_congr a
 
 -- ## Definition of ℤ and basic theorems and definitions
 
-definition int := image proj
+definition int [protected] := image proj
 notation `ℤ` := int
 
 definition psub : ℕ × ℕ → ℤ := fun_image proj
@@ -776,5 +776,5 @@ mul_ne_zero_left (mul_comm a b ▸ H)
 -- set_opaque lt true
 -- set_opaque sign true
 --transparent: sub ge gt
-
 end int -- namespace int
+abbreviation int := int.int