--- a/src/ZF/Epsilon.thy Sun Jun 24 11:41:41 2018 +0100
+++ b/src/ZF/Epsilon.thy Sun Jun 24 15:57:48 2018 +0200
@@ -5,7 +5,7 @@
section\<open>Epsilon Induction and Recursion\<close>
-theory Epsilon imports Nat_ZF begin
+theory Epsilon imports Nat begin
definition
eclose :: "i=>i" where