major code change: refute can now handle any Isabelle term, adds certain axioms automatically, and can handle inductive datatypes (but not yet recursion over them)
## targets
default: LNCS
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
USEDIR = $(ISATOOL) usedir -i true -d ps -D document -v true
## LNCS
LNCS: $(LOG)/HOL-LNCS.gz
$(LOG)/HOL-LNCS.gz: LNCS/ROOT.ML LNCS/document/root.tex LNCS/document/root.bib LNCS/*.thy
@$(USEDIR) HOL LNCS
## clean
clean:
@rm -f $(LOG)/HOL-LNCS.gz