From bcf15b0d39d87d64cd28d36ffaade6f674984428 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 15 Dec 2016 16:59:36 -0800
Subject: [PATCH] feat(library/init/data/int): import `int` by default

---
 library/init/data/default.lean     | 2 +-
 library/init/data/int/default.lean | 7 +++++++
 library/init/data/int/order.lean   | 3 ++-
 3 files changed, 10 insertions(+), 2 deletions(-)
 create mode 100644 library/init/data/int/default.lean

diff --git a/library/init/data/default.lean b/library/init/data/default.lean
index 6fd0e7a959..edbab1e2c3 100644
--- a/library/init/data/default.lean
+++ b/library/init/data/default.lean
@@ -5,4 +5,4 @@ Authors: Leonardo de Moura
 -/
 prelude
 import init.data.basic init.data.sigma init.data.nat init.data.char init.data.string
-import init.data.list init.data.sum init.data.subtype
+import init.data.list init.data.sum init.data.subtype init.data.int
diff --git a/library/init/data/int/default.lean b/library/init/data/int/default.lean
new file mode 100644
index 0000000000..fe5a3c761e
--- /dev/null
+++ b/library/init/data/int/default.lean
@@ -0,0 +1,7 @@
+/-
+Copyright (c) 2016 Microsoft Corporation. All rights reserved.
+Released under Apache 2.0 license as described in the file LICENSE.
+Authors: Leonardo de Moura
+-/
+prelude
+import init.data.int.basic init.data.int.order
diff --git a/library/init/data/int/order.lean b/library/init/data/int/order.lean
index eb8cf081c1..36faaf0fbb 100644
--- a/library/init/data/int/order.lean
+++ b/library/init/data/int/order.lean
@@ -5,7 +5,8 @@ Authors: Jeremy Avigad
 
 The order relation on the integers.
 -/
-import .basic
+prelude
+import init.data.int.basic
 
 namespace int