# HG changeset patch
# User paulson
# Date 813857576 -3600
# Node ID 92543c633f20571ae6c95bb2d903c0c2ffd6ed81
# Parent  68f6be60ab1c352d6f53aae8666524115021bdf1
Added the new Limit.{thy,ML} example

diff -r 68f6be60ab1c -r 92543c633f20 src/ZF/Makefile
--- 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)
 
diff -r 68f6be60ab1c -r 92543c633f20 src/ZF/ex/ROOT.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";