Fixed bug in dest_prem: premises of the form "p x_1 ... x_n"
(where p is a variable) are now treated as side conditions
if p is not in the list of (global) parameters.
#
# $Id$
#
# IsaMakefile for Cube
#
## targets
default: Pure-Cube
images:
test: Pure-Cube
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
## Pure-Cube
Pure-Cube: Pure $(LOG)/Pure-Cube.gz
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
Pure-Cube: Pure $(LOG)/Pure-Cube.gz
$(LOG)/Pure-Cube.gz: $(OUT)/Pure Cube.thy Example.thy ROOT.ML
@cd ..; $(ISATOOL) usedir $(OUT)/Pure Cube
## clean
clean:
@rm -f $(LOG)/Pure-Cube.gz