5621

1 
#


2 
# IsaMakefile for Tutorial


3 
#


4 


5 
## targets


6 


7 
default: HOLToyList HOLIfexpr HOLCodeGen HOLMisc


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 


22 


23 
## HOLIfexpr


24 


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


26 


27 
Ifexpr/Ifexpr.thy: Ifexpr/prolog Ifexpr/boolex Ifexpr/value Ifexpr/ifex \


28 
Ifexpr/valif Ifexpr/bool2if Ifexpr/normif Ifexpr/norm Ifexpr/normal \


29 
Ifexpr/end


30 
@cd Ifexpr; \


31 
cat prolog boolex value ifex valif bool2if normif norm normal \


32 
end > Ifexpr.thy


33 


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


35 
@$(ISATOOL) usedir $(OUT)/HOL Ifexpr


36 


37 


38 
## HOLToyList


39 


40 
HOLToyList: HOL $(LOG)/HOLToyList.gz


41 


42 
ToyList/ToyList.ML: ToyList/autotac ToyList/addsimps2 ToyList/inductxs \


43 
ToyList/lemma1 ToyList/lemma2 ToyList/lemma3 \


44 
ToyList/qed1 ToyList/qed2 ToyList/qed3 ToyList/thm ToyList/qed


45 
cd ToyList; \


46 
cat lemma2 inductxs autotac qed2 addsimps2 lemma3 qed3 \


47 
lemma1 inductxs autotac qed1 thm inductxs autotac qed > ToyList.ML


48 


49 
$(LOG)/HOLToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ToyList.ML \


50 
ToyList/ROOT.ML


51 
@$(ISATOOL) usedir $(OUT)/HOL ToyList


52 


53 
## HOLCodeGen


54 


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


56 


57 
CodeGen/CodeGen.thy: CodeGen/prolog CodeGen/expr CodeGen/value \


58 
CodeGen/instr CodeGen/exec CodeGen/comp CodeGen/end


59 
cd CodeGen; cat prolog expr value instr exec comp end > CodeGen.thy


60 


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


62 
CodeGen/goal2.ML CodeGen/simpsplit.ML CodeGen/ROOT.ML


63 
@$(ISATOOL) usedir $(OUT)/HOL CodeGen


64 


65 


66 
## HOLMisc


67 


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


69 


70 
Misc/Tree.thy: Misc/treeprolog Misc/tree Misc/end


71 
cd Misc; cat treeprolog tree end > Tree.thy


72 


73 
Misc/NatSum.thy: Misc/natsumprolog Misc/natsum Misc/end


74 
cd Misc; cat natsumprolog natsum end > NatSum.thy


75 


76 
Misc/Types.thy: Misc/typesprolog Misc/types Misc/end


77 
cd Misc; cat typesprolog types end > Types.thy


78 


79 
Misc/Defs.thy: Misc/defsprolog Misc/consts Misc/defs Misc/end


80 
cd Misc; cat defsprolog consts defs end > Defs.thy


81 


82 
Misc/ConstDefs.thy: Misc/constdefsprolog Misc/constdefs Misc/end


83 
cd Misc; cat constdefsprolog constdefs end > ConstDefs.thy


84 


85 
$(LOG)/HOLMisc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/exhaust.ML Misc/autotac.ML \


86 
Misc/Tree.thy Misc/NatSum.thy Misc/NatSum.ML Misc/Types.thy \


87 
Misc/Defs.thy Misc/ConstDefs.thy \


88 
Misc/Exor.thy Misc/exorgoal.ML Misc/exorproof.ML \


89 
Misc/splitif.ML Misc/splitlist.ML Misc/induct_auto.ML \


90 
Misc/Itrev.thy Misc/itrev1.ML Misc/itrev2.ML Misc/itrev3.ML


91 
@$(ISATOOL) usedir $(OUT)/HOL Misc


92 


93 


94 
## clean


95 


96 
clean:


97 
@rm f $(LOG)/HOLIfexpr.gz $(LOG)/HOLMisc.gz
