doc-src/IsarRef/IsaMakefile
author haftmann
Wed Sep 07 23:38:52 2011 +0200 (2011-09-07)
changeset 44818 27ba81ad0890
parent 42917 ba23e83b0868
permissions -rw-r--r--
theory of saturated naturals contributed by Peter Gammie
wenzelm@26738
     1
wenzelm@26738
     2
## targets
wenzelm@26738
     3
wenzelm@26840
     4
default: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
wenzelm@26738
     5
images: 
wenzelm@26840
     6
test: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
wenzelm@26738
     7
wenzelm@26738
     8
all: images test
wenzelm@26738
     9
wenzelm@26738
    10
wenzelm@26738
    11
## global settings
wenzelm@26738
    12
wenzelm@26738
    13
SRC = $(ISABELLE_HOME)/src
wenzelm@26738
    14
OUT = $(ISABELLE_OUTPUT)
wenzelm@26738
    15
LOG = $(OUT)/log
wenzelm@26738
    16
wenzelm@28500
    17
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
wenzelm@26738
    18
wenzelm@26738
    19
wenzelm@30456
    20
## sessions
wenzelm@26840
    21
wenzelm@26840
    22
HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
wenzelm@26738
    23
wenzelm@42651
    24
$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML Thy/Base.thy	\
wenzelm@29730
    25
  Thy/First_Order_Logic.thy Thy/Framework.thy Thy/Inner_Syntax.thy	\
wenzelm@42915
    26
  Thy/Preface.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy	\
wenzelm@29730
    27
  Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy		\
wenzelm@42917
    28
  Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Synopsis.thy		\
wenzelm@42917
    29
  Thy/Symbols.thy Thy/ML_Tactic.thy
wenzelm@26840
    30
	@$(USEDIR) -s IsarRef HOL Thy
wenzelm@30458
    31
	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
wenzelm@30458
    32
	 Thy/document/pdfsetup.sty Thy/document/session.tex
wenzelm@26840
    33
wenzelm@26738
    34
wenzelm@41729
    35
HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
wenzelm@26840
    36
wenzelm@27035
    37
$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML	\
wenzelm@42651
    38
  Thy/Base.thy Thy/HOLCF_Specific.thy
wenzelm@26840
    39
	@$(USEDIR) -s IsarRef -f ROOT-HOLCF.ML HOLCF Thy
wenzelm@30458
    40
	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
wenzelm@30458
    41
	 Thy/document/pdfsetup.sty Thy/document/session.tex
wenzelm@26840
    42
wenzelm@26840
    43
wenzelm@41729
    44
ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
wenzelm@26840
    45
wenzelm@42651
    46
$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML	\
wenzelm@42651
    47
  Thy/Base.thy Thy/ZF_Specific.thy
wenzelm@26840
    48
	@$(USEDIR) -s IsarRef -f ROOT-ZF.ML ZF Thy
wenzelm@30458
    49
	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
wenzelm@30458
    50
	 Thy/document/pdfsetup.sty Thy/document/session.tex
wenzelm@26738
    51
wenzelm@26738
    52
wenzelm@26738
    53
## clean
wenzelm@26738
    54
wenzelm@26738
    55
clean:
wenzelm@26840
    56
	@rm -f $(LOG)/HOL-IsarRef.gz $(LOG)/HOLCF-IsarRef.gz $(LOG)/ZF-IsarRef.gz