reverted slightly odd eb5900951702: isatest-doc should work again due to 4b08499b3db1 (polyml-5.3.0 supports proper TimeLimit, as required for HOL-Nitpick-Examples);
authorwenzelm
Tue, 08 Feb 2011 17:44:53 +0100
changeset 41729 ae1a46cdb9cb
parent 41728 2837df4d1c7a
child 41730 14ed42540d22
child 41735 bd7ee90267f2
reverted slightly odd eb5900951702: isatest-doc should work again due to 4b08499b3db1 (polyml-5.3.0 supports proper TimeLimit, as required for HOL-Nitpick-Examples);
doc-src/IsarRef/IsaMakefile
--- a/doc-src/IsarRef/IsaMakefile	Tue Feb 08 17:38:43 2011 +0100
+++ b/doc-src/IsarRef/IsaMakefile	Tue Feb 08 17:44:53 2011 +0100
@@ -31,10 +31,8 @@
 	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
 	 Thy/document/pdfsetup.sty Thy/document/session.tex
 
-HOLCF:
-	@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOLCF
 
-HOLCF-IsarRef: HOLCF $(LOG)/HOLCF-IsarRef.gz
+HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
 
 $(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML	\
   Thy/HOLCF_Specific.thy
@@ -42,10 +40,8 @@
 	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
 	 Thy/document/pdfsetup.sty Thy/document/session.tex
 
-ZF:
-	@cd $(SRC)/ZF; $(ISABELLE_TOOL) make ZF
 
-ZF-IsarRef: ZF $(LOG)/ZF-IsarRef.gz
+ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
 
 $(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML 		\
   Thy/ZF_Specific.thy