Modified dependencies for ex and Integ. (Rings)
authornipkow
Fri, 29 Nov 1996 15:07:27 +0100
changeset 2279 2f337bf81085
parent 2278 d63ffafce255
child 2280 eb2ba30c2981
Modified dependencies for ex and Integ. (Rings)
src/HOL/Makefile
--- a/src/HOL/Makefile	Fri Nov 29 12:22:22 1996 +0100
+++ b/src/HOL/Makefile	Fri Nov 29 15:07:27 1996 +0100
@@ -98,7 +98,7 @@
 	fi
 
 ##The integers in HOL
-INTEG_NAMES = Equiv Integ 
+INTEG_NAMES = Equiv Integ Group Ring Lagrange IntRingDefs IntRing
 
 INTEG_FILES = Integ/ROOT.ML \
 	      $(INTEG_NAMES:%=Integ/%.thy) $(INTEG_NAMES:%=Integ/%.ML)
@@ -198,7 +198,7 @@
 	fi
 
 ##Miscellaneous examples
-EX_NAMES = String BT Perm Comb InSort Qsort LexProd Group Ring Lagrange \
+EX_NAMES = String BT Perm Comb InSort Qsort LexProd \
 	   Puzzle Mutil Primes NatSum SList LList Acc PropLog Term Simult MT
 
 EX_FILES = ex/ROOT.ML ex/cla.ML ex/meson.ML ex/mesontest.ML ex/rel.ML \