author  wenzelm 
Sun, 15 Oct 2000 19:50:35 +0200  
changeset 10220  2a726de6e124 
parent 10217  e61e7e1eacaf 
child 10225  b9fd52525b69 
permissions  rwrr 
8743  1 
# 
2 
# IsaMakefile for Tutorial 

3 
# 

4 

5 
## targets 

6 

10217  7 
default: HOLToyList HOLIfexpr HOLCodeGen HOLTrie HOLDatatype HOLRecdef HOLAdvanced HOLCTL HOLInductive HOLMisc styles 
9520  8 
images: 
9 
test: 

10 
all: default 

8743  11 

12 

13 
## global settings 

14 

15 
SRC = $(ISABELLE_HOME)/src 

16 
OUT = $(ISABELLE_OUTPUT) 

17 
LOG = $(OUT)/log 

18 

19 

20 
## HOL 

21 

22 
HOL: 

23 
@cd $(SRC)/HOL; $(ISATOOL) make HOL 

24 

8825
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
wenzelm
parents:
8754
diff
changeset

25 
styles: 
8847  26 
@$(ISATOOL) latex o sty >/dev/null 
27 
@rm f pdfsetup.sty 

8825
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
wenzelm
parents:
8754
diff
changeset

28 
@rm f */document/isabelle.sty 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
wenzelm
parents:
8754
diff
changeset

29 
@rm f */document/isabellesym.sty 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
wenzelm
parents:
8754
diff
changeset

30 
@rm f */document/pdfsetup.sty 
10002  31 
@rm f */document/session.tex 
8743  32 

33 

34 
## HOLIfexpr 

35 

36 
HOLIfexpr: HOL $(LOG)/HOLIfexpr.gz 

37 

38 
$(LOG)/HOLIfexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML 

39 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Ifexpr 

8754  40 
@rm f tutorial.dvi 
8743  41 

42 
## HOLToyList 

43 

44 
HOLToyList: HOL $(LOG)/HOLToyList.gz $(LOG)/HOLToyList2.gz 

45 

46 
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 

47 
cat ToyList2/ToyList1 ToyList2/ToyList2 > ToyList2/ToyList.thy 

48 

49 
$(LOG)/HOLToyList2.gz: $(OUT)/HOL ToyList2/ToyList.thy ToyList2/ROOT.ML 

50 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL ToyList2 

8754  51 
@rm f tutorial.dvi 
8743  52 

53 
$(LOG)/HOLToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ROOT.ML 

54 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL ToyList 

8754  55 
@rm f tutorial.dvi 
8743  56 

57 
## HOLCodeGen 

58 

59 
HOLCodeGen: HOL $(LOG)/HOLCodeGen.gz 

60 

61 
$(LOG)/HOLCodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy 

62 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL CodeGen 

8754  63 
@rm f tutorial.dvi 
8743  64 

65 

66 
## HOLDatatype 

67 

68 
HOLDatatype: HOL $(LOG)/HOLDatatype.gz 

69 

8751  70 
$(LOG)/HOLDatatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \ 
9666  71 
Datatype/Nested.thy Datatype/unfoldnested.thy \ 
9644  72 
Datatype/Fundata.thy 
8743  73 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Datatype 
8754  74 
@rm f tutorial.dvi 
8743  75 

76 

77 
## HOLTrie 

78 

79 
HOLTrie: HOL $(LOG)/HOLTrie.gz 

80 

81 
$(LOG)/HOLTrie.gz: $(OUT)/HOL Trie/Option2.thy Trie/Trie.thy 

82 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Trie 

8754  83 
@rm f tutorial.dvi 
8743  84 

85 

86 
## HOLRecdef 

87 

88 
HOLRecdef: HOL $(LOG)/HOLRecdef.gz 

89 

10186  90 
$(LOG)/HOLRecdef.gz: $(OUT)/HOL Recdef/ROOT.ML Recdef/examples.thy Recdef/termination.thy \ 
9644  91 
Recdef/simplification.thy Recdef/Induction.thy \ 
10187  92 
Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy 
8743  93 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Recdef 
8754  94 
@rm f tutorial.dvi 
8743  95 

96 

9933  97 
## HOLAdvanced 
98 

99 
HOLAdvanced: HOL $(LOG)/HOLAdvanced.gz 

100 

10187  101 
$(LOG)/HOLAdvanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML Advanced/WFrec.thy 
9933  102 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Advanced 
103 
@rm f tutorial.dvi 

104 

9958  105 
## HOLCTL 
106 

107 
HOLCTL: HOL $(LOG)/HOLCTL.gz 

108 

10212  109 
$(LOG)/HOLCTL.gz: $(OUT)/HOL CTL/Base.thy CTL/PDL.thy CTL/CTL.thy CTL/CTLind.thy CTL/ROOT.ML 
9958  110 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL CTL 
111 
@rm f tutorial.dvi 

112 

10217  113 
## HOLInductive 
114 

115 
HOLInductive: HOL $(LOG)/HOLInductive.gz 

116 

117 
$(LOG)/HOLInductive.gz: $(OUT)/HOL Inductive/AB.thy Inductive/ROOT.ML 

118 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Inductive 

119 
@rm f tutorial.dvi 

120 

8743  121 
## HOLMisc 
122 

123 
HOLMisc: HOL $(LOG)/HOLMisc.gz 

124 

9722  125 
$(LOG)/HOLMisc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ 
9721  126 
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy \ 
127 
Misc/prime_def.thy Misc/case_exprs.thy \ 

9844  128 
Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy \ 
129 
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy 

8743  130 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Misc 
8754  131 
@rm f tutorial.dvi 
8743  132 

133 

134 
## clean 

135 

136 
clean: 

10217  137 
@rm f tutorial.dvi $(LOG)/HOLIfexpr.gz $(LOG)/HOLCodeGen.gz $(LOG)/HOLMisc.gz $(LOG)/HOLToyList.gz $(LOG)/HOLToyList2.gz $(LOG)/HOLTrie.gz $(LOG)/HOLDatatype.gz $(LOG)/HOLRecdef.gz $(LOG)/HOLAdvanced.gz $(LOG)/HOLCTL.gz $(LOG)/HOLInductive.gz 