author  wenzelm 
Mon, 08 May 2000 10:53:13 +0200  
changeset 8825  0c9cf33d499b 
parent 8754  42ce93ada11e 
child 8847  d6c92979fa51 
permissions  rwrr 
8743  1 
# 
2 
# IsaMakefile for Tutorial 

3 
# 

4 

5 
## targets 

6 

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

7 
default: HOLToyList HOLIfexpr HOLCodeGen HOLTrie HOLDatatype HOLRecdef HOLMisc styles 
8743  8 

9 

10 
## global settings 

11 

12 
SRC = $(ISABELLE_HOME)/src 

13 
OUT = $(ISABELLE_OUTPUT) 

14 
LOG = $(OUT)/log 

15 

16 

17 
## HOL 

18 

19 
HOL: 

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

21 

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

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

23 
@$(ISATOOL) latex o sty 
0c9cf33d499b
improved handling of Isabelle styles (less garbage);
wenzelm
parents:
8754
diff
changeset

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

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

26 
@rm f */document/pdfsetup.sty 
8743  27 

28 

29 
## HOLIfexpr 

30 

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

32 

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

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

8754  35 
@rm f tutorial.dvi 
8743  36 

37 
## HOLToyList 

38 

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

40 

41 
ToyList2/ToyList.thy: ToyList2/ToyList1 ToyList2/ToyList2 

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

43 

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

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

8754  46 
@rm f tutorial.dvi 
8743  47 

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

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

8754  50 
@rm f tutorial.dvi 
8743  51 

52 
## HOLCodeGen 

53 

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

55 

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

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

8754  58 
@rm f tutorial.dvi 
8743  59 

60 

61 
## HOLDatatype 

62 

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

64 

8751  65 
$(LOG)/HOLDatatype.gz: $(OUT)/HOL Datatype/ROOT.ML Datatype/ABexpr.thy \ 
66 
Datatype/Nested.thy Datatype/unfoldnested.thy Datatype/Fundata.thy 

8743  67 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Datatype 
8754  68 
@rm f tutorial.dvi 
8743  69 

70 

71 
## HOLTrie 

72 

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

74 

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

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

8754  77 
@rm f tutorial.dvi 
8743  78 

79 

80 
## HOLRecdef 

81 

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

83 

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

85 
Recdef/simplification.thy Recdef/Induction.thy 

86 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Recdef 

8754  87 
@rm f tutorial.dvi 
8743  88 

89 

90 
## HOLMisc 

91 

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

93 

94 
$(LOG)/HOLMisc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/cases.thy \ 

95 
Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/types.thy Misc/prime_def.thy \ 

96 
Misc/arith1.thy Misc/arith2.thy Misc/arith3.thy Misc/arith4.thy \ 

97 
Misc/def_rewr.thy Misc/let_rewr.thy Misc/cond_rewr.thy Misc/case_splits.thy \ 

98 
Misc/trace_simp.thy Misc/Itrev.thy Misc/asm_simp.thy 

99 
@$(ISATOOL) usedir i true d dvi D document $(OUT)/HOL Misc 

8754  100 
@rm f tutorial.dvi 
8743  101 

102 

103 
## clean 

104 

105 
clean: 

8754  106 
@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 