1. Myhill.thy is proved to correct some typos. 2. Some sections are added to the first direction. 3. The small theory of list difference is now separated into Prefix_subtract.thy and the ROOT.ML
## targets
default: ListP
images: ListP
test:
all: images test
## global settings
SRC = $(ISABELLE_HOME)/src
OUT = $(ISABELLE_OUTPUT)
LOG = $(OUT)/log
USEDIR = $(ISABELLE_TOOL) usedir -v true -i true -d pdf ## -D generated
## ListP
ListP: $(OUT)/ListP
$(OUT)/ListP: ROOT.ML document/root.tex *.thy
@$(USEDIR) -b HOL ListP
## clean
clean:
@rm -f $(OUT)/ListP