From 73aa024c3177da4b7b95a60665b7df9dde02f96b Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Sun, 5 Oct 2014 10:50:13 -0700
Subject: [PATCH] refactor(library/logic): remove 'core' subdirectory

---
 library/algebra/binary.lean                   |  2 +-
 library/algebra/category.lean                 |  2 +-
 library/algebra/relation.lean                 |  2 +-
 library/algebra/wf.lean                       |  5 ++--
 library/data/bool.lean                        |  2 +-
 library/data/empty.lean                       |  2 +-
 library/data/list/basic.lean                  |  1 -
 library/data/nat/basic.lean                   |  2 +-
 library/data/nat/order.lean                   |  2 +-
 library/data/num.lean                         |  2 +-
 library/data/option.lean                      |  2 +-
 library/data/prod.lean                        |  2 +-
 library/data/quotient/basic.lean              |  4 +--
 library/data/quotient/classical.lean          |  4 +--
 library/data/sigma.lean                       |  2 +-
 library/data/subtype.lean                     |  2 +-
 library/data/sum.lean                         |  2 +-
 library/data/unit.lean                        |  2 +-
 library/logic/axioms/classical.lean           |  2 +-
 library/logic/axioms/funext.lean              |  2 +-
 library/logic/axioms/hilbert.lean             |  4 +--
 library/logic/axioms/piext.lean               |  2 +-
 library/logic/axioms/prop_decidable.lean      |  2 +-
 library/logic/{core => }/cast.lean            |  0
 library/logic/{core => }/connectives.lean     |  0
 library/logic/core/core.md                    | 29 -------------------
 library/logic/core/examples/examples.md       |  4 ---
 library/logic/{core => }/decidable.lean       |  2 +-
 library/logic/default.lean                    | 10 +++----
 library/logic/{core => }/eq.lean              |  0
 library/logic/examples/examples.md            |  1 +
 .../{core => }/examples/instances_test.lean   |  0
 library/logic/{core => }/identities.lean      |  4 +--
 library/logic/{core => }/if.lean              |  2 +-
 library/logic/{core => }/inhabited.lean       |  2 +-
 library/logic/{core => }/instances.lean       |  2 +-
 library/logic/logic.md                        | 25 +++++++++++++++-
 library/logic/{core => }/nonempty.lean        |  0
 library/logic/{core => }/prop.lean            |  0
 library/logic/{core => }/quantifiers.lean     |  2 +-
 tests/lean/interactive/eq2.lean               |  2 +-
 tests/lean/interactive/findp.lean             |  2 +-
 tests/lean/interactive/num2.lean              |  2 +-
 tests/lean/run/cat.lean                       |  2 +-
 tests/lean/run/congr_imp_bug.lean             |  2 +-
 tests/lean/run/ctx.lean                       |  2 +-
 tests/lean/run/group3.lean                    |  2 +-
 tests/lean/run/sum_bug.lean                   |  4 +--
 tests/lean/run/tactic17.lean                  |  2 +-
 tests/lean/run/tt1.lean                       |  2 +-
 tests/lean/slow/cat_sec_var_bug.lean          |  2 +-
 51 files changed, 74 insertions(+), 87 deletions(-)
 rename library/logic/{core => }/cast.lean (100%)
 rename library/logic/{core => }/connectives.lean (100%)
 delete mode 100644 library/logic/core/core.md
 delete mode 100644 library/logic/core/examples/examples.md
 rename library/logic/{core => }/decidable.lean (99%)
 rename library/logic/{core => }/eq.lean (100%)
 rename library/logic/{core => }/examples/instances_test.lean (100%)
 rename library/logic/{core => }/identities.lean (97%)
 rename library/logic/{core => }/if.lean (98%)
 rename library/logic/{core => }/inhabited.lean (96%)
 rename library/logic/{core => }/instances.lean (98%)
 rename library/logic/{core => }/nonempty.lean (100%)
 rename library/logic/{core => }/prop.lean (100%)
 rename library/logic/{core => }/quantifiers.lean (98%)

diff --git a/library/algebra/binary.lean b/library/algebra/binary.lean
index 5979e00b74..5dfb4a8b60 100644
--- a/library/algebra/binary.lean
+++ b/library/algebra/binary.lean
@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic.core.eq
+import logic.eq
 open eq.ops
 
 namespace binary
diff --git a/library/algebra/category.lean b/library/algebra/category.lean
index 8c383c9f4d..52afce45eb 100644
--- a/library/algebra/category.lean
+++ b/library/algebra/category.lean
@@ -3,7 +3,7 @@
 -- Author: Floris van Doorn
 
 -- category
-import logic.core.eq logic.core.connectives
+import logic.eq logic.connectives
 import data.unit data.sigma data.prod
 import algebra.function
 import logic.axioms.funext
diff --git a/library/algebra/relation.lean b/library/algebra/relation.lean
index 1810fdb90d..065fe5a6c2 100644
--- a/library/algebra/relation.lean
+++ b/library/algebra/relation.lean
@@ -5,7 +5,7 @@
 -- algebra.relation
 -- ==============
 
-import logic.core.prop
+import logic.prop
 
 
 -- General properties of relations
diff --git a/library/algebra/wf.lean b/library/algebra/wf.lean
index 56d9cf79d7..c335f68104 100644
--- a/library/algebra/wf.lean
+++ b/library/algebra/wf.lean
@@ -1,9 +1,8 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-
-import logic.axioms.classical logic.axioms.prop_decidable logic.core.decidable
-import logic.core.identities
+import logic.identities logic.decidable
+import logic.axioms.classical logic.axioms.prop_decidable
 
 open decidable
 
diff --git a/library/data/bool.lean b/library/data/bool.lean
index c714ccf916..eda3725cce 100644
--- a/library/data/bool.lean
+++ b/library/data/bool.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 import general_notation
-import logic.core.connectives logic.core.decidable logic.core.inhabited
+import logic.connectives logic.decidable logic.inhabited
 
 open eq eq.ops decidable
 
diff --git a/library/data/empty.lean b/library/data/empty.lean
index 9d096c1d42..beb7e6e91e 100644
--- a/library/data/empty.lean
+++ b/library/data/empty.lean
@@ -5,7 +5,7 @@
 -- Empty type
 -- ----------
 
-import logic.core.cast
+import logic.cast
 
 inductive empty : Type
 
diff --git a/library/data/list/basic.lean b/library/data/list/basic.lean
index a4ba561ac9..f38b6f2e11 100644
--- a/library/data/list/basic.lean
+++ b/library/data/list/basic.lean
@@ -12,7 +12,6 @@
 import tools.tactic
 import data.nat
 import logic tools.helper_tactics
-import logic.core.identities
 
 open nat
 open eq.ops
diff --git a/library/data/nat/basic.lean b/library/data/nat/basic.lean
index 30ec6cf2ed..d7870783ea 100644
--- a/library/data/nat/basic.lean
+++ b/library/data/nat/basic.lean
@@ -8,7 +8,7 @@
 -- Basic operations on the natural numbers.
 
 import logic data.num tools.tactic algebra.binary tools.helper_tactics
-import logic.core.inhabited
+import logic.inhabited
 
 open tactic binary eq.ops
 open decidable
diff --git a/library/data/nat/order.lean b/library/data/nat/order.lean
index 7eb360d186..1173f9f1de 100644
--- a/library/data/nat/order.lean
+++ b/library/data/nat/order.lean
@@ -7,7 +7,7 @@
 --
 -- The ordering on the natural numbers
 
-import .basic logic.core.decidable
+import .basic logic.decidable
 import tools.fake_simplifier
 
 open nat eq.ops tactic
diff --git a/library/data/num.lean b/library/data/num.lean
index f12ade6d58..8b7f47f3c5 100644
--- a/library/data/num.lean
+++ b/library/data/num.lean
@@ -3,7 +3,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
-import logic.core.inhabited data.bool general_notation
+import logic.inhabited data.bool general_notation
 open bool
 
 -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
diff --git a/library/data/option.lean b/library/data/option.lean
index a289bd9190..c152106b9d 100644
--- a/library/data/option.lean
+++ b/library/data/option.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.core.eq logic.core.inhabited logic.core.decidable
+import logic.eq logic.inhabited logic.decidable
 open eq.ops decidable
 
 inductive option (A : Type) : Type :=
diff --git a/library/data/prod.lean b/library/data/prod.lean
index 1e50f26fef..4e4931a044 100644
--- a/library/data/prod.lean
+++ b/library/data/prod.lean
@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
-import logic.core.inhabited logic.core.eq logic.core.decidable
+import logic.inhabited logic.eq logic.decidable
 
 -- data.prod
 -- =========
diff --git a/library/data/quotient/basic.lean b/library/data/quotient/basic.lean
index f29e56b7f9..5bb091a942 100644
--- a/library/data/quotient/basic.lean
+++ b/library/data/quotient/basic.lean
@@ -5,8 +5,8 @@
 -- Theory data.quotient
 -- ====================
 
-import logic tools.tactic ..subtype logic.core.cast algebra.relation data.prod
-import logic.core.instances
+import logic tools.tactic data.subtype logic.cast algebra.relation data.prod
+import logic.instances
 import .util
 
 open relation prod inhabited nonempty tactic eq.ops
diff --git a/library/data/quotient/classical.lean b/library/data/quotient/classical.lean
index e8a61751e2..cc17afef6a 100644
--- a/library/data/quotient/classical.lean
+++ b/library/data/quotient/classical.lean
@@ -2,9 +2,9 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Floris van Doorn
 
-import algebra.relation logic.core.nonempty data.subtype
-import .basic
+import algebra.relation logic.nonempty data.subtype
 import logic.axioms.classical logic.axioms.hilbert logic.axioms.funext
+import .basic
 
 namespace quotient
 
diff --git a/library/data/sigma.lean b/library/data/sigma.lean
index ef45bfbfbc..6c4ee4a5de 100644
--- a/library/data/sigma.lean
+++ b/library/data/sigma.lean
@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad, Floris van Doorn
-import logic.core.inhabited logic.core.eq
+import logic.inhabited logic.eq
 open inhabited eq.ops
 
 inductive sigma {A : Type} (B : A → Type) : Type :=
diff --git a/library/data/subtype.lean b/library/data/subtype.lean
index 2dff44a116..c0420e85c4 100644
--- a/library/data/subtype.lean
+++ b/library/data/subtype.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
 
-import logic.core.inhabited logic.core.eq logic.core.decidable
+import logic.inhabited logic.eq logic.decidable
 
 open decidable
 
diff --git a/library/data/sum.lean b/library/data/sum.lean
index ee628eb688..1c818771b7 100644
--- a/library/data/sum.lean
+++ b/library/data/sum.lean
@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
-import logic.core.prop logic.core.inhabited logic.core.decidable
+import logic.prop logic.inhabited logic.decidable
 open inhabited decidable eq.ops
 -- data.sum
 -- ========
diff --git a/library/data/unit.lean b/library/data/unit.lean
index b768cfee62..4cca0914b3 100644
--- a/library/data/unit.lean
+++ b/library/data/unit.lean
@@ -1,7 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
-import logic.core.decidable logic.core.inhabited
+import logic.decidable logic.inhabited
 open decidable
 
 inductive unit : Type :=
diff --git a/library/logic/axioms/classical.lean b/library/logic/axioms/classical.lean
index f2a560e4af..26a8b3f4a5 100644
--- a/library/logic/axioms/classical.lean
+++ b/library/logic/axioms/classical.lean
@@ -5,7 +5,7 @@
 -- logic.axioms.classical
 -- ======================
 
-import logic.core.quantifiers logic.core.cast algebra.relation
+import logic.quantifiers logic.cast algebra.relation
 
 open eq.ops
 
diff --git a/library/logic/axioms/funext.lean b/library/logic/axioms/funext.lean
index 36d1185821..28070a71ca 100644
--- a/library/logic/axioms/funext.lean
+++ b/library/logic/axioms/funext.lean
@@ -5,7 +5,7 @@
 -- logic.axioms.funext
 -- ===================
 
-import logic.core.eq algebra.function
+import logic.eq algebra.function
 open function
 
 -- Function extensionality
diff --git a/library/logic/axioms/hilbert.lean b/library/logic/axioms/hilbert.lean
index a288ff0d24..90ee81068a 100644
--- a/library/logic/axioms/hilbert.lean
+++ b/library/logic/axioms/hilbert.lean
@@ -8,8 +8,8 @@
 -- Follows Coq.Logic.ClassicalEpsilon (but our definition of "inhabited" is the
 -- constructive one).
 
-import logic.core.quantifiers
-import logic.core.inhabited logic.core.nonempty
+import logic.quantifiers
+import logic.inhabited logic.nonempty
 import data.subtype data.sum
 
 open subtype inhabited nonempty
diff --git a/library/logic/axioms/piext.lean b/library/logic/axioms/piext.lean
index fec2676c97..b80110a38c 100644
--- a/library/logic/axioms/piext.lean
+++ b/library/logic/axioms/piext.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.core.inhabited logic.core.cast
+import logic.inhabited logic.cast
 
 open inhabited
 
diff --git a/library/logic/axioms/prop_decidable.lean b/library/logic/axioms/prop_decidable.lean
index 8bbdec34e7..63b16a0231 100644
--- a/library/logic/axioms/prop_decidable.lean
+++ b/library/logic/axioms/prop_decidable.lean
@@ -5,7 +5,7 @@
 -- logic.axioms.prop_decidable
 -- ===========================
 
-import logic.axioms.classical logic.axioms.hilbert logic.core.decidable
+import logic.axioms.classical logic.axioms.hilbert logic.decidable
 open decidable inhabited nonempty
 
 -- Excluded middle + Hilbert implies every proposition is decidable
diff --git a/library/logic/core/cast.lean b/library/logic/cast.lean
similarity index 100%
rename from library/logic/core/cast.lean
rename to library/logic/cast.lean
diff --git a/library/logic/core/connectives.lean b/library/logic/connectives.lean
similarity index 100%
rename from library/logic/core/connectives.lean
rename to library/logic/connectives.lean
diff --git a/library/logic/core/core.md b/library/logic/core/core.md
deleted file mode 100644
index ca8cf3cda6..0000000000
--- a/library/logic/core/core.md
+++ /dev/null
@@ -1,29 +0,0 @@
-logic.core
-==========
-
-Logical operations and connectives.
-
-* [prop](prop.lean) : the type Prop
-* [eq](eq.lean) : equality and disequality
-* [connectives](connectives.lean) : propositional connectives
-* [cast](cast.lean) : casts and heterogeneous equality
-* [quantifiers](quantifiers.lean) : existential and universal quantifiers
-* [if](if.lean) : if-then-else
-* [identities](identities.lean) : some useful identities
-* [examples](examples/examples.md)
-
-Type classes for general logical manipulations:
-
-* [inhabited](inhabited.lean) : inhabited types
-* [nonempty](nonempty.lean) : nonempty type
-* [decidable](decidable.lean) : decidable types
-* [instances](instances.lean) : type class instances
-
-Constructively, inhabited types have a witness, while nonempty types
-are "proof irrelevant". Classically (assuming the axioms in
-logic.axioms.hilbert) the two are equivalent. Type class inferences
-are set up to use "inhabited" however, so users should use that to
-declare that types have an element. Use "nonempty" in the hypothesis
-of a theorem when the theorem does not depend on the witness chosen.
-
-
diff --git a/library/logic/core/examples/examples.md b/library/logic/core/examples/examples.md
deleted file mode 100644
index 6f6962b60e..0000000000
--- a/library/logic/core/examples/examples.md
+++ /dev/null
@@ -1,4 +0,0 @@
-logic.connectives.examples
-==========================
-
-* [instances_test](instances_test.lean)
diff --git a/library/logic/core/decidable.lean b/library/logic/decidable.lean
similarity index 99%
rename from library/logic/core/decidable.lean
rename to library/logic/decidable.lean
index 44c373e7bb..cf76b746d0 100644
--- a/library/logic/core/decidable.lean
+++ b/library/logic/decidable.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 
-import logic.core.connectives
+import logic.connectives
 
 inductive decidable (p : Prop) : Type :=
 inl : p  → decidable p,
diff --git a/library/logic/default.lean b/library/logic/default.lean
index 3b3b5ad161..85b31f3792 100644
--- a/library/logic/default.lean
+++ b/library/logic/default.lean
@@ -2,8 +2,8 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 
-import logic.core.connectives logic.core.eq logic.core.cast 
-import logic.core.quantifiers logic.core.if 
-import logic.core.decidable logic.core.inhabited logic.core.nonempty
-import logic.core.instances
-import logic.core.identities
+import logic.connectives logic.eq logic.cast
+import logic.quantifiers logic.if
+import logic.decidable logic.inhabited logic.nonempty
+import logic.instances
+import logic.identities
diff --git a/library/logic/core/eq.lean b/library/logic/eq.lean
similarity index 100%
rename from library/logic/core/eq.lean
rename to library/logic/eq.lean
diff --git a/library/logic/examples/examples.md b/library/logic/examples/examples.md
index 8cf5cdde41..22d5c532b2 100644
--- a/library/logic/examples/examples.md
+++ b/library/logic/examples/examples.md
@@ -2,3 +2,4 @@ logic.examples
 ==============
 
 * [nuprl_examples](nuprl_examples.lean) : examples from "Logical investigations with the Nuprl Proof Assistant"
+* [instances_test](instances_test.lean)
diff --git a/library/logic/core/examples/instances_test.lean b/library/logic/examples/instances_test.lean
similarity index 100%
rename from library/logic/core/examples/instances_test.lean
rename to library/logic/examples/instances_test.lean
diff --git a/library/logic/core/identities.lean b/library/logic/identities.lean
similarity index 97%
rename from library/logic/core/identities.lean
rename to library/logic/identities.lean
index e142c1aa11..d5f48b79e4 100644
--- a/library/logic/core/identities.lean
+++ b/library/logic/identities.lean
@@ -2,13 +2,13 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Jeremy Avigad, Leonardo de Moura
 
--- logic.connectives.identities
+-- logic.identities
 -- ============================
 
 -- Useful logical identities. In the absence of propositional extensionality, some of the
 -- calculations use the type class support provided by logic.connectives.instances
 
-import logic.core.instances logic.core.decidable logic.core.quantifiers logic.core.cast
+import logic.instances logic.decidable logic.quantifiers logic.cast
 
 open relation decidable relation.iff_ops
 
diff --git a/library/logic/core/if.lean b/library/logic/if.lean
similarity index 98%
rename from library/logic/core/if.lean
rename to library/logic/if.lean
index aba58ebab4..e11b4a26ee 100644
--- a/library/logic/core/if.lean
+++ b/library/logic/if.lean
@@ -4,7 +4,7 @@
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
 
-import logic.core.decidable tools.tactic
+import logic.decidable tools.tactic
 open decidable tactic eq.ops
 
 definition ite (c : Prop) {H : decidable c} {A : Type} (t e : A) : A :=
diff --git a/library/logic/core/inhabited.lean b/library/logic/inhabited.lean
similarity index 96%
rename from library/logic/core/inhabited.lean
rename to library/logic/inhabited.lean
index f03db1ec39..23e6728005 100644
--- a/library/logic/core/inhabited.lean
+++ b/library/logic/inhabited.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import logic.core.connectives
+import logic.connectives
 
 inductive inhabited (A : Type) : Type :=
 mk : A → inhabited A
diff --git a/library/logic/core/instances.lean b/library/logic/instances.lean
similarity index 98%
rename from library/logic/core/instances.lean
rename to library/logic/instances.lean
index ed63800b1b..6c991d10e8 100644
--- a/library/logic/core/instances.lean
+++ b/library/logic/instances.lean
@@ -5,7 +5,7 @@
 -- logic.core.instances
 -- ====================
 
-import logic.core.connectives algebra.relation
+import logic.connectives algebra.relation
 
 namespace relation
 
diff --git a/library/logic/logic.md b/library/logic/logic.md
index 8a74e1abd5..8397c18fd5 100644
--- a/library/logic/logic.md
+++ b/library/logic/logic.md
@@ -4,6 +4,29 @@ logic
 Logical constructions and axioms. By default, `import logic` does not
 import any additional axioms.
 
-* [core](core/core.md) : logical connectives and type classes
+Logical operations and connectives.
+
+* [prop](prop.lean) : the type Prop
+* [eq](eq.lean) : equality and disequality
+* [connectives](connectives.lean) : propositional connectives
+* [cast](cast.lean) : casts and heterogeneous equality
+* [quantifiers](quantifiers.lean) : existential and universal quantifiers
+* [if](if.lean) : if-then-else
+* [identities](identities.lean) : some useful identities
+
+Type classes for general logical manipulations:
+
+* [inhabited](inhabited.lean) : inhabited types
+* [nonempty](nonempty.lean) : nonempty type
+* [decidable](decidable.lean) : decidable types
+* [instances](instances.lean) : type class instances
+
+Constructively, inhabited types have a witness, while nonempty types
+are "proof irrelevant". Classically (assuming the axioms in
+logic.axioms.hilbert) the two are equivalent. Type class inferences
+are set up to use "inhabited" however, so users should use that to
+declare that types have an element. Use "nonempty" in the hypothesis
+of a theorem when the theorem does not depend on the witness chosen.
+
 * [axioms](axioms/axioms.md) : additional axioms
 * [examples](examples/examples.md)
\ No newline at end of file
diff --git a/library/logic/core/nonempty.lean b/library/logic/nonempty.lean
similarity index 100%
rename from library/logic/core/nonempty.lean
rename to library/logic/nonempty.lean
diff --git a/library/logic/core/prop.lean b/library/logic/prop.lean
similarity index 100%
rename from library/logic/core/prop.lean
rename to library/logic/prop.lean
diff --git a/library/logic/core/quantifiers.lean b/library/logic/quantifiers.lean
similarity index 98%
rename from library/logic/core/quantifiers.lean
rename to library/logic/quantifiers.lean
index 9b37fa47d4..605a87cf5e 100644
--- a/library/logic/core/quantifiers.lean
+++ b/library/logic/quantifiers.lean
@@ -2,7 +2,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Authors: Leonardo de Moura, Jeremy Avigad
 
-import .connectives ..core.nonempty
+import logic.connectives logic.nonempty
 
 open inhabited nonempty
 
diff --git a/tests/lean/interactive/eq2.lean b/tests/lean/interactive/eq2.lean
index a96cdd9831..6b70b38a71 100644
--- a/tests/lean/interactive/eq2.lean
+++ b/tests/lean/interactive/eq2.lean
@@ -7,7 +7,7 @@
 
 -- Equality.
 
-import logic.core.prop
+import logic.prop
 
 -- eq
 -- --
diff --git a/tests/lean/interactive/findp.lean b/tests/lean/interactive/findp.lean
index d69089c247..223b3287c3 100644
--- a/tests/lean/interactive/findp.lean
+++ b/tests/lean/interactive/findp.lean
@@ -1,4 +1,4 @@
-import logic.core.eq algebra.relation
+import logic.eq algebra.relation
 
 check proof_irrel
 
diff --git a/tests/lean/interactive/num2.lean b/tests/lean/interactive/num2.lean
index b5b38d6d55..21342523ab 100644
--- a/tests/lean/interactive/num2.lean
+++ b/tests/lean/interactive/num2.lean
@@ -3,7 +3,7 @@
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura
 ----------------------------------------------------------------------------------------------------
-import logic.core.inhabited
+import logic.inhabited
 
 -- pos_num and num are two auxiliary datatypes used when parsing numerals such as 13, 0, 26.
 -- The parser will generate the terms (pos (bit1 (bit1 (bit0 one)))), zero, and (pos (bit0 (bit1 (bit1 one)))).
diff --git a/tests/lean/run/cat.lean b/tests/lean/run/cat.lean
index 02da97756b..e8a3e79683 100644
--- a/tests/lean/run/cat.lean
+++ b/tests/lean/run/cat.lean
@@ -3,7 +3,7 @@
 -- Author: Floris van Doorn
 
 -- category
-import logic.core.eq logic.core.connectives
+import logic.eq logic.connectives
 import data.unit data.sigma data.prod
 import algebra.function
 
diff --git a/tests/lean/run/congr_imp_bug.lean b/tests/lean/run/congr_imp_bug.lean
index 3b1f7f1974..a0955cd2e3 100644
--- a/tests/lean/run/congr_imp_bug.lean
+++ b/tests/lean/run/congr_imp_bug.lean
@@ -3,7 +3,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 ----------------------------------------------------------------------------------------------------
-import logic.core.connectives algebra.function
+import logic.connectives algebra.function
 open function
 
 namespace congr
diff --git a/tests/lean/run/ctx.lean b/tests/lean/run/ctx.lean
index ec2a83049a..ce2499270b 100644
--- a/tests/lean/run/ctx.lean
+++ b/tests/lean/run/ctx.lean
@@ -1,4 +1,4 @@
-import data.nat logic.core.inhabited
+import data.nat logic.inhabited
 open nat inhabited
 
 constant N : Type.{1}
diff --git a/tests/lean/run/group3.lean b/tests/lean/run/group3.lean
index 9d17285e20..3921a8eba0 100644
--- a/tests/lean/run/group3.lean
+++ b/tests/lean/run/group3.lean
@@ -7,7 +7,7 @@
 
 -- Various structures with 1, *, inv, including groups.
 
-import logic.core.eq logic.core.connectives
+import logic.eq logic.connectives
 import data.unit data.sigma data.prod
 import algebra.function algebra.binary
 
diff --git a/tests/lean/run/sum_bug.lean b/tests/lean/run/sum_bug.lean
index f14030ec8d..0fd288e168 100644
--- a/tests/lean/run/sum_bug.lean
+++ b/tests/lean/run/sum_bug.lean
@@ -1,9 +1,7 @@
 -- Copyright (c) 2014 Microsoft Corporation. All rights reserved.
 -- Released under Apache 2.0 license as described in the file LICENSE.
 -- Author: Leonardo de Moura, Jeremy Avigad
-
-import logic.core.prop logic.core.inhabited logic.core.decidable
-
+import logic.prop logic.inhabited logic.decidable
 open inhabited decidable
 
 -- TODO: take this outside the namespace when the inductive package handles it better
diff --git a/tests/lean/run/tactic17.lean b/tests/lean/run/tactic17.lean
index f4c89853d4..962d0afe41 100644
--- a/tests/lean/run/tactic17.lean
+++ b/tests/lean/run/tactic17.lean
@@ -5,6 +5,6 @@ constant A : Type.{1}
 constant f : A → A → A
 
 theorem tst {a b c : A} (H1 : a = b) (H2 : b = c) : f a b = f b c
-:= by apply (@congr A A (f a) (f b));
+:= by apply (@congr A A _ _ (f a) (f b));
       apply (congr_arg f);
       !assumption
diff --git a/tests/lean/run/tt1.lean b/tests/lean/run/tt1.lean
index 4753423a55..c8a30b6683 100644
--- a/tests/lean/run/tt1.lean
+++ b/tests/lean/run/tt1.lean
@@ -1,4 +1,4 @@
-import data.prod data.num logic.core.quantifiers
+import data.prod data.num logic.quantifiers
 open prod
 
 check (true, false, 10)
diff --git a/tests/lean/slow/cat_sec_var_bug.lean b/tests/lean/slow/cat_sec_var_bug.lean
index 943114e60f..599d4828fc 100644
--- a/tests/lean/slow/cat_sec_var_bug.lean
+++ b/tests/lean/slow/cat_sec_var_bug.lean
@@ -3,7 +3,7 @@
 -- Author: Floris van Doorn
 
 -- category
-import logic.core.eq logic.core.connectives
+import logic.eq logic.connectives
 import data.unit data.sigma data.prod
 import algebra.function
 import logic.axioms.funext