src/HOL/IsaMakefile
changeset 33449 9a4b176292ec
parent 33447 6895b9cadc7c
parent 33448 7f716a975ada
child 33450 4389ec600ba7
equal deleted inserted replaced
33447:6895b9cadc7c 33449:9a4b176292ec
   661   Algebra/poly/PolyHomo.thy \
   661   Algebra/poly/PolyHomo.thy \
   662   Algebra/poly/Polynomial.thy \
   662   Algebra/poly/Polynomial.thy \
   663   Algebra/poly/UnivPoly2.thy \
   663   Algebra/poly/UnivPoly2.thy \
   664   Algebra/ringsimp.ML
   664   Algebra/ringsimp.ML
   665 
   665 
   666 $(LOG)/HOL-Algebra.gz: $(ALGEBRA_DEPENDENCIES)
   666 $(OUT)/HOL-Algebra: $(ALGEBRA_DEPENDENCIES)
   667 	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
   667 	@cd Algebra; $(ISABELLE_TOOL) usedir -b -g true -V outline=/proof,/ML $(OUT)/HOL HOL-Algebra
   668 
   668 
   669 
   669 
   670 ## HOL-Auth
   670 ## HOL-Auth
   671 
   671