# HG changeset patch
# User nipkow
# Date 849276447 -3600
# Node ID 2f337bf8108539af6b36d6b8db0606eb22be1488
# Parent  d63ffafce255988ae0c360842ee80f0f3a43a1ce
Modified dependencies for ex and Integ. (Rings)

diff -r d63ffafce255 -r 2f337bf81085 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 \