--- a/src/ZF/ex/Limit.thy Sun Apr 09 20:17:00 2017 +0200
+++ b/src/ZF/ex/Limit.thy Sun Apr 09 20:44:35 2017 +0200
@@ -17,7 +17,7 @@
Laboratory, 1995.
*)
-theory Limit imports Main begin
+theory Limit imports ZF begin
definition
rel :: "[i,i,i]=>o" where