added cheating, sorry_text (from skip_proofs.ML);
added method_setup (from isar_thy.ML);
#
# $Id$
#
# IsaMakefile for Cube
#
## targets
default: Cube
images: Cube
test: Cube-ex
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
## Cube
Cube: Pure $(OUT)/Cube
Pure:
@cd $(SRC)/Pure; $(ISATOOL) make Pure
$(OUT)/Cube: $(OUT)/Pure Cube.thy ROOT.ML
@$(ISATOOL) usedir -b $(OUT)/Pure Cube
## Cube-ex
Cube-ex: Cube $(LOG)/Cube-ex.gz
$(LOG)/Cube-ex.gz: $(OUT)/Cube ex/ex.thy ex/ROOT.ML
@$(ISATOOL) usedir $(OUT)/Cube ex
## clean
clean:
@rm -f $(OUT)/Cube $(LOG)/Cube.gz $(LOG)/Cube-ex.gz