doc-src/TutorialI/Overview/IsaMakefile
author chaieb
Wed, 19 May 2004 11:23:59 +0200
changeset 14758 af3b71a46a1c
parent 13439 2f98365f57a8
child 28500 4b79e5d3d0aa
permissions -rw-r--r--
A new implementation for presburger arithmetic following the one suggested in technical report Chaieb Amine and Tobias Nipkow. It is generic an smaller. the tactic has also changed and allows the abstaction over fuction occurences whose type is nat or int.
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
13263
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
     1
## targets
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
     2
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
     3
default: LNCS
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
     4
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
     5
## global settings
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
     6
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
     7
SRC = $(ISABELLE_HOME)/src
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
     8
OUT = $(ISABELLE_OUTPUT)
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
     9
LOG = $(OUT)/log
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    10
USEDIR = $(ISATOOL) usedir -i true -d ps -D document -v true
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    11
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    12
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    13
## LNCS
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    14
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    15
LNCS: $(LOG)/HOL-LNCS.gz
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    16
13439
2f98365f57a8 *** empty log message ***
nipkow
parents: 13263
diff changeset
    17
$(LOG)/HOL-LNCS.gz: LNCS/ROOT.ML LNCS/document/root.tex LNCS/document/root.bib LNCS/*.thy
13263
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    18
	@$(USEDIR) HOL LNCS
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    19
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    20
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    21
## clean
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    22
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    23
clean:
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    24
	@rm -f $(LOG)/HOL-LNCS.gz
203c5f789c09 *** empty log message ***
nipkow
parents:
diff changeset
    25