# HG changeset patch
# User paulson
# Date 988878424 -7200
# Node ID aaa0ad8fea6b29fad4dd3b2f9747e2f9213287d2
# Parent  9710486b886b35e3c5385c55b2dfd257976d5f50
remove unnecessary TeX files

diff -r 9710486b886b -r aaa0ad8fea6b doc-src/TutorialI/IsaMakefile
--- a/doc-src/TutorialI/IsaMakefile	Wed May 02 11:54:18 2001 +0200
+++ b/doc-src/TutorialI/IsaMakefile	Thu May 03 10:27:04 2001 +0200
@@ -36,6 +36,8 @@
 	@rm -f */document/isabellesym.sty
 	@rm -f */document/pdfsetup.sty
 	@rm -f */document/session.tex
+	@rm -f Rules/document/*.tex
+	@rm -f Sets/document/*.tex
 
 
 ## HOL-Ifexpr