doc-src/Exercises/2003/IsaMakefile
author obua
Sun, 09 May 2004 23:04:36 +0200
changeset 14722 8e739a6eaf11
parent 14524 0ccba84113a1
permissions -rw-r--r--
replaced apply-style proof for instance Multiset :: plus_ac0 by recommended Isar proof style
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
14524
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
     1
#
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
     2
# $Id$
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
     3
#
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
     4
# IsaMakefile for PSV2003
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
     5
#
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
     6
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
     7
SESSIONS = a1 a2 a3 a5 a6
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
     8
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
     9
## targets
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    10
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    11
default: clean sessions
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    12
sessions: $(SESSIONS)
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    13
# all: sessions 
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    14
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    15
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    16
## global settings
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    17
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    18
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    19
SRC = $(ISABELLE_HOME)/src
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    20
OUT = $(ISABELLE_OUTPUT)
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    21
LOG = $(OUT)/log
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    22
INFO = $(ISABELLE_BROWSER_INFO)
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    23
USEDIR = $(ISATOOL) usedir -v true -i false -d false -D generated
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    24
RSYNC = rsync --rsh ssh --rsync-path /usr/local/dist/bin/rsync
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    25
WWW = www4.in.tum.de:/home/html/wbroy/html-data/lehre/praktika/psv
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    26
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    27
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    28
# reomve old log files
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    29
clean:
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    30
	rm -f $(LOG)/HOL-a?.gz $(LOG)/HOL-l?.gz
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    31
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    32
## provide style.tex
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    33
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    34
style:
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    35
	@for D in $(SESSIONS); do test -d $$D/document && { test -r $$D/document/style.tex || ln -s ../../style.tex $$D/document/style.tex; } done;
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    36
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    37
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    38
## a1
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    39
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    40
a1: a1/generated/session.tex
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    41
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    42
a1/generated/session.tex: a1/ROOT.ML \
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    43
  a1/*.thy
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    44
	@$(USEDIR) HOL a1
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    45
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    46
## a2
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    47
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    48
a2: a2/generated/session.tex
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    49
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    50
a2/generated/session.tex: a2/ROOT.ML \
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    51
  a2/*.thy
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    52
	@$(USEDIR) HOL a2
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    53
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    54
## a3
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    55
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    56
a3: a3/generated/session.tex
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    57
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    58
a3/generated/session.tex: a3/ROOT.ML \
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    59
  a3/*.thy
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    60
	@$(USEDIR) HOL a3
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    61
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    62
## a5
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    63
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    64
a5: a5/generated/session.tex
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    65
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    66
a5/generated/session.tex: a5/ROOT.ML \
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    67
  a5/*.thy
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    68
	@$(USEDIR) HOL a5
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    69
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    70
## a6
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    71
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    72
 a6: a6/generated/session.tex
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    73
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    74
 a6/generated/session.tex: a6/ROOT.ML \
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    75
   a6/*.thy
0ccba84113a1 *** empty log message ***
mehta
parents:
diff changeset
    76
	@$(USEDIR) HOL a6