# HG changeset patch # User nipkow # Date 907759310 -7200 # Node ID 1fe18aca1062a548441f41e9b96ff557999faf4a # Parent 3ac11c4af76ae009e6a95728a727ccba75aced2e runs test diff -r 3ac11c4af76a -r 1fe18aca1062 doc-src/Tutorial/IsaMakefile --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/doc-src/Tutorial/IsaMakefile Wed Oct 07 13:21:50 1998 +0200 @@ -0,0 +1,97 @@ +# +# IsaMakefile for Tutorial +# + +## targets + +default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Misc + + +## global settings + +SRC = $(ISABELLE_HOME)/src +OUT = $(ISABELLE_OUTPUT) +LOG = $(OUT)/log + + +## HOL + +HOL: + @cd $(SRC)/HOL; $(ISATOOL) make HOL + + +## HOL-Ifexpr + +HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz + +Ifexpr/Ifexpr.thy: Ifexpr/prolog Ifexpr/boolex Ifexpr/value Ifexpr/ifex \ + Ifexpr/valif Ifexpr/bool2if Ifexpr/normif Ifexpr/norm Ifexpr/normal \ + Ifexpr/end + @cd Ifexpr; \ + cat prolog boolex value ifex valif bool2if normif norm normal \ + end > Ifexpr.thy + +$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML + @$(ISATOOL) usedir $(OUT)/HOL Ifexpr + + +## HOL-ToyList + +HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz + +ToyList/ToyList.ML: ToyList/autotac ToyList/addsimps2 ToyList/inductxs \ + ToyList/lemma1 ToyList/lemma2 ToyList/lemma3 \ + ToyList/qed1 ToyList/qed2 ToyList/qed3 ToyList/thm ToyList/qed + cd ToyList; \ + cat lemma2 inductxs autotac qed2 addsimps2 lemma3 qed3 \ + lemma1 inductxs autotac qed1 thm inductxs autotac qed > ToyList.ML + +$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ToyList.ML \ + ToyList/ROOT.ML + @$(ISATOOL) usedir $(OUT)/HOL ToyList + +## HOL-CodeGen + +HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz + +CodeGen/CodeGen.thy: CodeGen/prolog CodeGen/expr CodeGen/value \ + CodeGen/instr CodeGen/exec CodeGen/comp CodeGen/end + cd CodeGen; cat prolog expr value instr exec comp end > CodeGen.thy + +$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy CodeGen/goal1.ML \ + CodeGen/goal2.ML CodeGen/simpsplit.ML CodeGen/ROOT.ML + @$(ISATOOL) usedir $(OUT)/HOL CodeGen + + +## HOL-Misc + +HOL-Misc: HOL $(LOG)/HOL-Misc.gz + +Misc/Tree.thy: Misc/treeprolog Misc/tree Misc/end + cd Misc; cat treeprolog tree end > Tree.thy + +Misc/NatSum.thy: Misc/natsumprolog Misc/natsum Misc/end + cd Misc; cat natsumprolog natsum end > NatSum.thy + +Misc/Types.thy: Misc/typesprolog Misc/types Misc/end + cd Misc; cat typesprolog types end > Types.thy + +Misc/Defs.thy: Misc/defsprolog Misc/consts Misc/defs Misc/end + cd Misc; cat defsprolog consts defs end > Defs.thy + +Misc/ConstDefs.thy: Misc/constdefsprolog Misc/constdefs Misc/end + cd Misc; cat constdefsprolog constdefs end > ConstDefs.thy + +$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/exhaust.ML Misc/autotac.ML \ + Misc/Tree.thy Misc/NatSum.thy Misc/NatSum.ML Misc/Types.thy \ + Misc/Defs.thy Misc/ConstDefs.thy \ + Misc/Exor.thy Misc/exorgoal.ML Misc/exorproof.ML \ + Misc/splitif.ML Misc/splitlist.ML Misc/induct_auto.ML \ + Misc/Itrev.thy Misc/itrev1.ML Misc/itrev2.ML Misc/itrev3.ML + @$(ISATOOL) usedir $(OUT)/HOL Misc + + +## clean + +clean: + @rm -f $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-Misc.gz