--- /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