# HG changeset patch
# User paulson
# Date 941802337 -3600
# Node ID 7acf6eb8eec1d2a004ff84c8de5b92ca802ce74d
# Parent  3d0c34795831eb4d23c02558bd843a74f809cf57
Algebra and Polynomial theories, by Clemens Ballarin

diff -r 3d0c34795831 -r 7acf6eb8eec1 src/HOL/IsaMakefile
--- a/src/HOL/IsaMakefile	Fri Nov 05 11:14:26 1999 +0100
+++ b/src/HOL/IsaMakefile	Fri Nov 05 12:45:37 1999 +0100
@@ -8,7 +8,7 @@
 
 default: HOL
 images: HOL HOL-Real TLA
-test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex \
+test: HOL-Subst HOL-Induct HOL-IMP HOL-Hoare HOL-Lex HOL-Algebra \
   HOL-Auth HOL-UNITY HOL-Modelcheck HOL-Lambda HOL-W0 HOL-MiniML HOL-BCV \
   HOL-IOA HOL-AxClasses-Group HOL-AxClasses-Lattice \
   HOL-AxClasses-Tutorial HOL-Quot HOL-ex HOL-Isar_examples HOL-Real-ex \
@@ -178,6 +178,28 @@
 	@$(ISATOOL) usedir $(OUT)/HOL Lex
 
 
+## HOL-Algebra
+
+HOL-Algebra: HOL $(LOG)/HOL-Algebra.gz
+
+$(LOG)/HOL-Algebra.gz: $(OUT)/HOL Algebra/ROOT.ML \
+  Algebra/abstract/Abstract.thy \
+  Algebra/abstract/Factor.ML Algebra/abstract/Factor.thy \
+  Algebra/abstract/Field.thy \
+  Algebra/abstract/Ideal.ML Algebra/abstract/Ideal.thy \
+  Algebra/abstract/NatSum.ML Algebra/abstract/NatSum.thy \
+  Algebra/abstract/PID.thy \
+  Algebra/abstract/Ring.ML Algebra/abstract/Ring.thy \
+  Algebra/abstract/RingHomo.ML Algebra/abstract/RingHomo.thy\
+  Algebra/poly/Degree.ML Algebra/poly/Degree.thy \
+  Algebra/poly/LongDiv.ML Algebra/poly/LongDiv.thy \
+  Algebra/poly/PolyHomo.ML Algebra/poly/PolyHomo.thy \
+  Algebra/poly/PolyRing.ML Algebra/poly/PolyRing.thy \
+  Algebra/poly/Polynomial.thy \
+  Algebra/poly/ProtoPoly.ML Algebra/poly/ProtoPoly.thy \
+  Algebra/poly/UnivPoly.ML Algebra/poly/UnivPoly.thy
+	@$(ISATOOL) usedir $(OUT)/HOL Algebra
+
 ## HOL-Auth
 
 HOL-Auth: HOL $(LOG)/HOL-Auth.gz