Added the new Limit.{thy,ML} example
authorpaulson
Mon, 16 Oct 1995 16:32:56 +0100
changeset 1282 92543c633f20
parent 1281 68f6be60ab1c
child 1283 ea8b657a9c92
Added the new Limit.{thy,ML} example
src/ZF/Makefile
src/ZF/ex/ROOT.ML
--- 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";