added an intro lemma for freshness of products; set up
the simplifier so that it can deal with the compact and
long notation for freshness constraints (FIXME: it should
also be able to deal with the special case of freshness
of atoms)
## targets
default: Locales
images:
test: Locales
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
USEDIR = $(ISATOOL) usedir -d false -D document
## Locales
Locales: $(LOG)/HOL-Locales.gz
HOL:
@cd $(SRC)/HOL; $(ISATOOL) make HOL
$(LOG)/HOL-Locales.gz: $(OUT)/HOL Locales/ROOT.ML Locales/Locales.thy \
Locales/document/root.tex Locales/document/root.bib
@$(USEDIR) $(OUT)/HOL Locales
## clean
clean:
@rm -f $(LOG)/HOL-Locales.gz