added Induct/Binary_Trees.thy, Induct/Tree_Forest (converted from
former ex/TF.ML ex/TF.thy ex/Term.ML ex/Term.thy);
#
# $Id$
#
## targets
default: HOL-datatype
images:
test: HOL-datatype
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
## HOL-datatype
HOL:
@cd $(SRC)/HOL; $(ISATOOL) make HOL
HOL-datatype: HOL $(LOG)/HOL-datatype.gz
$(LOG)/HOL-datatype.gz: $(OUT)/HOLBrackin.thy Instructions.thy SML.thy \
Verilog.thy
@cd ..; $(ISATOOL) usedir -s HOL-datatype $(OUT)/HOL HOL-datatype
## clean
clean:
@rm -f $(LOG)/HOL-datatype.gz