Admin/Benchmarks/HOL-datatype/IsaMakefile
author paulson
Wed, 25 Jul 2001 18:21:01 +0200
changeset 11455 e07927b980ec
parent 7372 79e911c0c7d1
child 32965 ecb746bca732
permissions -rw-r--r--
defer_recdef (lazyR_def) now looks for theorem Hilbert_Choice.tfl_some dynamically, so recdef no longer needs to import Hilbert_Choice.

#
# $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