--- a/src/ZF/Makefile Mon Oct 16 14:56:24 1995 +0100
+++ b/src/ZF/Makefile Mon Oct 16 16:32:56 1995 +0100
@@ -96,8 +96,8 @@
echo 'exit_use"Resid/ROOT.ML";quit();' | $(LOGIC)
##Miscellaneous examples
-EX_NAMES = Ramsey Integ twos_compl Bin BT Term TF Ntree Brouwer Data Enum \
- Rmap PropLog ListN Acc Comb Primrec LList CoUnit
+EX_NAMES = Ramsey Limit Integ twos_compl Bin BT Term TF Ntree Brouwer \
+ Data Enum Rmap PropLog ListN Acc Comb Primrec LList CoUnit
EX_FILES = ex/ROOT.ML ex/misc.ML $(EX_NAMES:%=ex/%.thy) $(EX_NAMES:%=ex/%.ML)
--- 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";