--- a/doc-src/TutorialI/IsaMakefile Sun May 01 16:36:34 2011 +0200
+++ b/doc-src/TutorialI/IsaMakefile Sun May 01 16:52:29 2011 +0200
@@ -6,7 +6,7 @@
default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Trie HOL-Datatype HOL-Fun HOL-Fun \
HOL-Advanced HOL-Rules HOL-Sets HOL-CTL HOL-Inductive HOL-Types HOL-Misc \
- HOL-Protocol HOL-Documents styles
+ HOL-Protocol HOL-Documents
images:
test:
all: default
@@ -26,17 +26,6 @@
HOL:
@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
-styles:
- @rm -f isabelle.sty
- @rm -f isabellesym.sty
- @rm -f pdfsetup.sty
- @$(ISABELLE_TOOL) latex -o sty >/dev/null
- @rm -f pdfsetup.sty
- @rm -f */document/isabelle.sty
- @rm -f */document/isabellesym.sty
- @rm -f */document/pdfsetup.sty
- @rm -f */document/session.tex
-
## HOL-Ifexpr
@@ -45,6 +34,10 @@
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
$(USEDIR) Ifexpr
+ @rm -f Ifexpr/document/isabelle.sty
+ @rm -f Ifexpr/document/isabellesym.sty
+ @rm -f Ifexpr/document/pdfsetup.sty
+ @rm -f Ifexpr/document/session.tex
@rm -f tutorial.dvi
## HOL-ToyList
@@ -56,10 +49,18 @@
$(LOG)/HOL-ToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML
$(USEDIR) ToyList2
+ @rm -f ToyList2/document/isabelle.sty
+ @rm -f ToyList2/document/isabellesym.sty
+ @rm -f ToyList2/document/pdfsetup.sty
+ @rm -f ToyList2/document/session.tex
@rm -f tutorial.dvi
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML
$(USEDIR) ToyList
+ @rm -f ToyList/document/isabelle.sty
+ @rm -f ToyList/document/isabellesym.sty
+ @rm -f ToyList/document/pdfsetup.sty
+ @rm -f ToyList/document/session.tex
@rm -f tutorial.dvi
## HOL-CodeGen
@@ -68,6 +69,10 @@
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/ROOT.ML CodeGen/CodeGen.thy
$(USEDIR) CodeGen
+ @rm -f CodeGen/document/isabelle.sty
+ @rm -f CodeGen/document/isabellesym.sty
+ @rm -f CodeGen/document/pdfsetup.sty
+ @rm -f CodeGen/document/session.tex
@rm -f tutorial.dvi
@@ -79,6 +84,10 @@
Datatype/Nested.thy Datatype/unfoldnested.thy \
Datatype/Fundata.thy
$(USEDIR) Datatype
+ @rm -f Datatype/document/isabelle.sty
+ @rm -f Datatype/document/isabellesym.sty
+ @rm -f Datatype/document/pdfsetup.sty
+ @rm -f Datatype/document/session.tex
@rm -f tutorial.dvi
@@ -88,6 +97,10 @@
$(LOG)/HOL-Trie.gz: $(OUT)/HOL Trie/ROOT.ML Trie/Trie.thy
$(USEDIR) Trie
+ @rm -f Trie/document/isabelle.sty
+ @rm -f Trie/document/isabellesym.sty
+ @rm -f Trie/document/pdfsetup.sty
+ @rm -f Trie/document/session.tex
@rm -f tutorial.dvi
@@ -97,6 +110,10 @@
$(LOG)/HOL-Fun.gz: $(OUT)/HOL Fun/ROOT.ML Fun/fun0.thy
$(USEDIR) Fun
+ @rm -f Fun/document/isabelle.sty
+ @rm -f Fun/document/isabellesym.sty
+ @rm -f Fun/document/pdfsetup.sty
+ @rm -f Fun/document/session.tex
@rm -f tutorial.dvi
@@ -106,6 +123,10 @@
$(LOG)/HOL-Advanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML
$(USEDIR) Advanced
+ @rm -f Advanced/document/isabelle.sty
+ @rm -f Advanced/document/isabellesym.sty
+ @rm -f Advanced/document/pdfsetup.sty
+ @rm -f Advanced/document/session.tex
@rm -f tutorial.dvi
## HOL-Rules
@@ -116,6 +137,10 @@
Rules/Blast.thy Rules/Force.thy Rules/Primes.thy Rules/Forward.thy \
Rules/Tacticals.thy Rules/find2.thy Rules/ROOT.ML
@$(USEDIR) Rules
+ @rm -f Rules/document/isabelle.sty
+ @rm -f Rules/document/isabellesym.sty
+ @rm -f Rules/document/pdfsetup.sty
+ @rm -f Rules/document/session.tex
@rm -f tutorial.dvi
## HOL-Sets
@@ -125,6 +150,10 @@
$(LOG)/HOL-Sets.gz: $(OUT)/HOL Sets/Examples.thy Sets/Functions.thy \
Sets/Recur.thy Sets/Relations.thy Sets/ROOT.ML
@$(USEDIR) Sets
+ @rm -f Sets/document/isabelle.sty
+ @rm -f Sets/document/isabellesym.sty
+ @rm -f Sets/document/pdfsetup.sty
+ @rm -f Sets/document/session.tex
@rm -f tutorial.dvi
## HOL-CTL
@@ -133,6 +162,10 @@
$(LOG)/HOL-CTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML
$(USEDIR) CTL
+ @rm -f CTL/document/isabelle.sty
+ @rm -f CTL/document/isabellesym.sty
+ @rm -f CTL/document/pdfsetup.sty
+ @rm -f CTL/document/session.tex
@rm -f tutorial.dvi
## HOL-Inductive
@@ -143,6 +176,10 @@
Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \
Inductive/Advanced.thy
$(USEDIR) Inductive
+ @rm -f Inductive/document/isabelle.sty
+ @rm -f Inductive/document/isabellesym.sty
+ @rm -f Inductive/document/pdfsetup.sty
+ @rm -f Inductive/document/session.tex
@rm -f tutorial.dvi
## HOL-Types
@@ -153,6 +190,10 @@
Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedefs.thy \
Types/Overloading.thy Types/Axioms.thy
$(USEDIR) Types
+ @rm -f Types/document/isabelle.sty
+ @rm -f Types/document/isabellesym.sty
+ @rm -f Types/document/pdfsetup.sty
+ @rm -f Types/document/session.tex
@rm -f tutorial.dvi
## HOL-Misc
@@ -164,6 +205,10 @@
Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy
$(USEDIR) Misc
+ @rm -f Misc/document/isabelle.sty
+ @rm -f Misc/document/isabellesym.sty
+ @rm -f Misc/document/pdfsetup.sty
+ @rm -f Misc/document/session.tex
@rm -f tutorial.dvi
@@ -175,6 +220,10 @@
Protocol/Message.thy Protocol/Event.thy \
Protocol/Public.thy Protocol/NS_Public.thy
$(USEDIR) Protocol
+ @rm -f Protocol/document/isabelle.sty
+ @rm -f Protocol/document/isabellesym.sty
+ @rm -f Protocol/document/pdfsetup.sty
+ @rm -f Protocol/document/session.tex
@rm -f tutorial.dvi
## HOL-Documents
@@ -183,6 +232,10 @@
$(LOG)/HOL-Documents.gz: $(OUT)/HOL Documents/Documents.thy Documents/ROOT.ML
$(USEDIR) Documents
+ @rm -f Documents/document/isabelle.sty
+ @rm -f Documents/document/isabellesym.sty
+ @rm -f Documents/document/pdfsetup.sty
+ @rm -f Documents/document/session.tex
@rm -f tutorial.dvi
## clean