From 781f709bb4e599e9cd07c97a4dcd21dbb833d8b2 Mon Sep 17 00:00:00 2001
From: Leonardo de Moura <leonardo@microsoft.com>
Date: Thu, 6 Nov 2014 15:03:13 -0800
Subject: [PATCH] feat(library/logic): import wf.lean in logic/default.lean

We will use well-founded recursion in the definitional package
---
 library/logic/default.lean  | 2 +-
 tests/lean/acc.lean         | 2 +-
 tests/lean/acc_rec_bug.lean | 2 +-
 3 files changed, 3 insertions(+), 3 deletions(-)

diff --git a/library/logic/default.lean b/library/logic/default.lean
index 85b31f3792..5f21f0e1b1 100644
--- a/library/logic/default.lean
+++ b/library/logic/default.lean
@@ -2,7 +2,7 @@
 --- Released under Apache 2.0 license as described in the file LICENSE.
 --- Author: Jeremy Avigad
 
-import logic.connectives logic.eq logic.cast
+import logic.connectives logic.eq logic.cast logic.wf
 import logic.quantifiers logic.if
 import logic.decidable logic.inhabited logic.nonempty
 import logic.instances
diff --git a/tests/lean/acc.lean b/tests/lean/acc.lean
index eb4fe2db06..aa49023d7c 100644
--- a/tests/lean/acc.lean
+++ b/tests/lean/acc.lean
@@ -1,4 +1,4 @@
-import logic
+import logic.prop
 
 inductive acc (A : Type) (R : A → A → Prop) :  A → Prop :=
 intro : ∀ (x : A), (∀ (y : A), R y x → acc A R y) → acc A R x
diff --git a/tests/lean/acc_rec_bug.lean b/tests/lean/acc_rec_bug.lean
index dfb454f3fd..57dcdb9806 100644
--- a/tests/lean/acc_rec_bug.lean
+++ b/tests/lean/acc_rec_bug.lean
@@ -1,4 +1,4 @@
-import logic
+import logic.prop
 
 inductive acc {A : Type} (R : A → A → Prop) : A → Prop :=
 intro : ∀x, (∀ y, R y x → acc R y) → acc R x