author  nipkow 
Tue, 12 Sep 2000 15:43:15 +0200  
changeset 9933  9feb1e0c4cb3 
parent 9844  8016321c7de1 
child 9958  67f2920862c7 
permissions  rwrr 
8743  1 
# 
2 
# IsaMakefile for Tutorial 

3 
# 

4 

5 
## targets 

6 

9933  7 
default: HOLToyList HOLIfexpr HOLCodeGen HOLTrie HOLDatatype HOLRecdef HOLAdvanced 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 
8743  31 

32 

33 
## HOLIfexpr 

34 

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

36 

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

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

8754  39 
@rm f tutorial.dvi 
8743  40 

41 
## HOLToyList 

42 

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

44 

45 
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 

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

47 

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

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

8754  50 
@rm f tutorial.dvi 
8743  51 

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

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

8754  54 
@rm f tutorial.dvi 
8743  55 

56 
## HOLCodeGen 

57 

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

59 

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

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

8754  62 
@rm f tutorial.dvi 
8743  63 

64 

65 
## HOLDatatype 

66 

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

68 

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

75 

76 
## HOLTrie 

77 

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

79 

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

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

8754  82 
@rm f tutorial.dvi 
8743  83 

84 

85 
## HOLRecdef 

86 

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

88 

89 
$(LOG)/HOLRecdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \ 

9644  90 
Recdef/simplification.thy Recdef/Induction.thy \ 
9689  91 
Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy 
8743  92 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Recdef 
8754  93 
@rm f tutorial.dvi 
8743  94 

95 

9933  96 
## HOLAdvanced 
97 

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

99 

100 
$(LOG)/HOLAdvanced.gz: $(OUT)/HOL Advanced/simp.thy Advanced/ROOT.ML 

101 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Advanced 

102 
@rm f tutorial.dvi 

103 

8743  104 
## HOLMisc 
105 

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

107 

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

9844  111 
Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy \ 
112 
Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy 

8743  113 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Misc 
8754  114 
@rm f tutorial.dvi 
8743  115 

116 

117 
## clean 

118 

119 
clean: 

9933  120 
@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 