--- a/doc-src/Tutorial/IsaMakefile Mon Nov 29 11:23:48 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,144 +0,0 @@
-#
-# IsaMakefile for Tutorial
-#
-
-## targets
-
-default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Recdef HOL-Misc
-images:
-test:
-all: default
-
-
-## 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-Datatype
-
-HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
-
-Datatype/appmap.ML: Datatype/appmap
- cat Datatype/goal Datatype/appmap Datatype/semi > Datatype/appmap.ML
-
-Datatype/ABexp.thy: Datatype/abprolog Datatype/abdata Datatype/abconstseval \
- Datatype/abevala Datatype/abevalb Datatype/abconstssubst Datatype/absubsta\
- Datatype/absubstb
- cd Datatype; cat abprolog abdata abconstseval abevala abevalb abconstssubst absubsta absubstb end > ABexp.thy
-
-Datatype/Term.thy: Datatype/tprolog Datatype/mutnested Datatype/tdata \
- Datatype/tconstssubst Datatype/tsubst Datatype/tsubsts
- cd Datatype; cat tprolog mutnested tdata tconstssubst tsubst tsubsts end > Term.thy
-
-Datatype/Trie.thy: Datatype/trieprolog Datatype/assoc Datatype/trie \
- Datatype/triesels Datatype/lookup Datatype/update
- cd Datatype; cat trieprolog assoc trie triesels lookup update end > Trie.thy
-
-$(LOG)/HOL-Datatype.gz: $(OUT)/HOL \
- Datatype/ABexp.thy Datatype/Term.thy Datatype/Trie.thy \
- Datatype/ROOT.ML Datatype/abgoalind.ML Datatype/autotac.ML \
- Datatype/tidproof.ML Datatype/appmap.ML Datatype/lookupempty.ML \
- Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML
- @$(ISATOOL) usedir $(OUT)/HOL Datatype
-
-## HOL-Recdef
-
-HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
-
-Recdef/Examples.thy: Recdef/exprolog Recdef/fib Recdef/sep Recdef/last \
- Recdef/constsgcd Recdef/gcd Recdef/ack
- cd Recdef; cat exprolog fib sep last constsgcd gcd ack end > Examples.thy
-
-Recdef/Sep1.thy: Recdef/sep1prolog Recdef/sep1
- cd Recdef; cat sep1prolog sep1 end > Sep1.thy
-
-Recdef/Sep2.thy: Recdef/sep2prolog Recdef/sep2
- cd Recdef; cat sep2prolog sep2 end > Sep2.thy
-
-$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML \
- Recdef/Examples.thy Recdef/Sep1.thy Recdef/Sep2.thy
- @$(ISATOOL) usedir $(OUT)/HOL Recdef
-
-## 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
--- a/doc-src/Tutorial/Makefile Mon Nov 29 11:23:48 2004 +0100
+++ /dev/null Thu Jan 01 00:00:00 1970 +0000
@@ -1,37 +0,0 @@
-#
-# $Id$
-#
-
-## targets
-
-default: dvi
-
-
-## dependencies
-
-include ../Makefile.in
-
-NAME = tutorial
-FILES = tutorial.tex basics.tex fp.tex appendix.tex \
- ../iman.sty ../ttbox.sty ../extra.sty
-
-dvi: $(NAME).dvi
-
-$(NAME).dvi: $(FILES) isabelle_hol.eps
- $(LATEX) $(NAME)
- $(BIBTEX) $(NAME)
- $(LATEX) $(NAME)
- $(LATEX) $(NAME)
- $(SEDINDEX) $(NAME)
- $(LATEX) $(NAME)
-
-pdf: $(NAME).pdf
-
-$(NAME).pdf: $(FILES) isabelle_hol.pdf
- $(PDFLATEX) $(NAME)
- $(BIBTEX) $(NAME)
- $(PDFLATEX) $(NAME)
- $(PDFLATEX) $(NAME)
- $(SEDINDEX) $(NAME)
- $(FIXBOOKMARKS) $(NAME).out
- $(PDFLATEX) $(NAME)