doc-src/ProgProve/IsaMakefile
author wenzelm
Tue, 03 Apr 2012 20:37:52 +0200
changeset 47319 8aa23a259ab2
parent 47269 29aa0c071875
permissions -rw-r--r--
prefer static dependencies;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     1
## targets
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     2
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     3
default: HOL-ProgProve
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     4
images:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     5
test: HOL-ProgProve
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     6
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     7
all: images test
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     8
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
     9
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    10
## global settings
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    11
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    12
SRC = $(ISABELLE_HOME)/src
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    13
OUT = $(ISABELLE_OUTPUT)
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    14
LOG = $(OUT)/log
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    15
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    16
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    17
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    18
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    19
## sessions
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    20
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    21
HOL-ProgProve: $(LOG)/HOL-ProgProve.gz
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    22
47319
8aa23a259ab2 prefer static dependencies;
wenzelm
parents: 47269
diff changeset
    23
$(LOG)/HOL-ProgProve.gz: \
8aa23a259ab2 prefer static dependencies;
wenzelm
parents: 47269
diff changeset
    24
  Thys/Basics.thy \
8aa23a259ab2 prefer static dependencies;
wenzelm
parents: 47269
diff changeset
    25
  Thys/Bool_nat_list.thy \
8aa23a259ab2 prefer static dependencies;
wenzelm
parents: 47269
diff changeset
    26
  Thys/Isar.thy \
8aa23a259ab2 prefer static dependencies;
wenzelm
parents: 47269
diff changeset
    27
  Thys/LaTeXsugar.thy \
8aa23a259ab2 prefer static dependencies;
wenzelm
parents: 47269
diff changeset
    28
  Thys/Logic.thy \
8aa23a259ab2 prefer static dependencies;
wenzelm
parents: 47269
diff changeset
    29
  Thys/MyList.thy \
8aa23a259ab2 prefer static dependencies;
wenzelm
parents: 47269
diff changeset
    30
  Thys/Types_and_funs.thy \
8aa23a259ab2 prefer static dependencies;
wenzelm
parents: 47269
diff changeset
    31
  Thys/ROOT.ML
47269
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    32
	@$(USEDIR) -s ProgProve HOL Thys
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    33
	@rm -f Thys/document/MyList.tex
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    34
	@rm -f Thys/document/isabelle.sty
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    35
	@rm -f Thys/document/isabellesym.sty
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    36
	@rm -f Thys/document/pdfsetup.sty
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    37
	@rm -f Thys/document/railsetup.sty
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    38
	@rm -f Thys/document/session.tex
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    39
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    40
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    41
## clean
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    42
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    43
clean:
29aa0c071875 New manual Programming and Proving in Isabelle/HOL
nipkow
parents:
diff changeset
    44
	@rm -f $(LOG)/HOL-ProgProve.gz