fixed a printing problem for bounded quantifiers and bounded set operators in the case of tuples
## targets
default: all
images:
test: HOL-datatype HOL-record
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
## HOL-datatype
HOL:
@cd $(SRC)/HOL; $(ISABELLE_TOOL) make HOL
HOL-datatype: HOL $(LOG)/HOL-datatype.gz
$(LOG)/HOL-datatype.gz: $(OUT)/HOL HOL-datatype/ROOT.ML \
HOL-datatype/Brackin.thy HOL-datatype/Instructions.thy \
HOL-datatype/SML.thy HOL-datatype/Verilog.thy
@$(ISABELLE_TOOL) usedir -s datatype $(OUT)/HOL HOL-datatype
## HOL-record
HOL-record: HOL $(LOG)/HOL-record.gz
$(LOG)/HOL-record.gz: $(OUT)/HOL HOL-record/ROOT.ML \
HOL-record/RecordBenchmark.thy
@$(ISABELLE_TOOL) usedir -s record $(OUT)/HOL HOL-record
## clean
clean:
@rm -f $(LOG)/HOL-datatype.gz $(LOG)/HOL-record.gz