Admin/Benchmarks/IsaMakefile
author wenzelm
Mon, 13 Mar 2000 13:21:39 +0100
changeset 8434 5e4bba59bfaa
parent 7371 b176626f0d80
child 10099 44da60e5331b
permissions -rw-r--r--
use HOLogic.Not; export indexify_names;

#
# $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)/HOL HOL-datatype/Brackin.thy \
  HOL-datatype/Instructions.thy HOL-datatype/SML.thy \
  HOL-datatype/Verilog.thy
	$(ISATOOL) usedir -s HOL-datatype $(OUT)/HOL HOL-datatype


## clean

clean:
	@rm -f $(LOG)/HOL-datatype.gz