src/ZF/ex/ROOT.ML
changeset 1282 92543c633f20
parent 960 358a19a91d52
child 1296 ae31bb7774a7
--- a/src/ZF/ex/ROOT.ML	Mon Oct 16 14:56:24 1995 +0100
+++ b/src/ZF/ex/ROOT.ML	Mon Oct 16 16:32:56 1995 +0100
@@ -15,6 +15,7 @@
 
 time_use     "ex/misc.ML";
 time_use_thy "ex/Ramsey";
+time_use_thy "ex/Limit";
 
 (*Integers & Binary integer arithmetic*)
 time_use_thy "ex/Bin";