doc-src/IsarRef/IsaMakefile
author blanchet
Mon, 19 Apr 2010 18:14:45 +0200
changeset 36230 43d10a494c91
parent 30458 804de935c328
child 41721 eb5900951702
permissions -rw-r--r--
added warning about inconsistent context to Metis; it makes more sense here than in Sledgehammer, because Sledgehammer is unsound and there's no point in having people panicking about the consistency of their context when their context is in fact consistent
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     1
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     2
## targets
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     3
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
     4
default: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     5
images: 
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
     6
test: HOL-IsarRef HOLCF-IsarRef ZF-IsarRef
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     7
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     8
all: images test
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
     9
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    10
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    11
## global settings
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    12
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    13
SRC = $(ISABELLE_HOME)/src
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    14
OUT = $(ISABELLE_OUTPUT)
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    15
LOG = $(OUT)/log
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    16
28500
4b79e5d3d0aa replaced ISATOOL by ISABELLE_TOOL;
wenzelm
parents: 27048
diff changeset
    17
USEDIR = $(ISABELLE_TOOL) usedir -v true -i false -d false -C false -D document
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    18
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    19
30456
wenzelm
parents: 30242
diff changeset
    20
## sessions
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    21
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    22
HOL-IsarRef: $(LOG)/HOL-IsarRef.gz
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    23
27035
d038a2ba87f6 renamed theory "intro" to "Introduction";
wenzelm
parents: 26869
diff changeset
    24
$(LOG)/HOL-IsarRef.gz: Thy/ROOT.ML ../antiquote_setup.ML		\
29730
924c1fd5f303 added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents: 29716
diff changeset
    25
  Thy/First_Order_Logic.thy Thy/Framework.thy Thy/Inner_Syntax.thy	\
924c1fd5f303 added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents: 29716
diff changeset
    26
  Thy/Introduction.thy Thy/Outer_Syntax.thy Thy/Spec.thy Thy/Proof.thy	\
924c1fd5f303 added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents: 29716
diff changeset
    27
  Thy/Misc.thy Thy/Document_Preparation.thy Thy/Generic.thy		\
924c1fd5f303 added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents: 29716
diff changeset
    28
  Thy/HOL_Specific.thy Thy/Quick_Reference.thy Thy/Symbols.thy		\
924c1fd5f303 added example "First-Order Logic" -- mostly from Trybulec Festschrift;
wenzelm
parents: 29716
diff changeset
    29
  Thy/ML_Tactic.thy
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    30
	@$(USEDIR) -s IsarRef HOL Thy
30458
804de935c328 delete unused generated files;
wenzelm
parents: 30456
diff changeset
    31
	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
804de935c328 delete unused generated files;
wenzelm
parents: 30456
diff changeset
    32
	 Thy/document/pdfsetup.sty Thy/document/session.tex
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    33
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    34
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    35
HOLCF-IsarRef: $(LOG)/HOLCF-IsarRef.gz
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    36
27035
d038a2ba87f6 renamed theory "intro" to "Introduction";
wenzelm
parents: 26869
diff changeset
    37
$(LOG)/HOLCF-IsarRef.gz: Thy/ROOT-HOLCF.ML ../antiquote_setup.ML	\
d038a2ba87f6 renamed theory "intro" to "Introduction";
wenzelm
parents: 26869
diff changeset
    38
  Thy/HOLCF_Specific.thy
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    39
	@$(USEDIR) -s IsarRef -f ROOT-HOLCF.ML HOLCF Thy
30458
804de935c328 delete unused generated files;
wenzelm
parents: 30456
diff changeset
    40
	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
804de935c328 delete unused generated files;
wenzelm
parents: 30456
diff changeset
    41
	 Thy/document/pdfsetup.sty Thy/document/session.tex
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    42
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    43
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    44
ZF-IsarRef: $(LOG)/ZF-IsarRef.gz
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    45
27035
d038a2ba87f6 renamed theory "intro" to "Introduction";
wenzelm
parents: 26869
diff changeset
    46
$(LOG)/ZF-IsarRef.gz: Thy/ROOT-ZF.ML ../antiquote_setup.ML 		\
d038a2ba87f6 renamed theory "intro" to "Introduction";
wenzelm
parents: 26869
diff changeset
    47
  Thy/ZF_Specific.thy
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    48
	@$(USEDIR) -s IsarRef -f ROOT-ZF.ML ZF Thy
30458
804de935c328 delete unused generated files;
wenzelm
parents: 30456
diff changeset
    49
	@rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \
804de935c328 delete unused generated files;
wenzelm
parents: 30456
diff changeset
    50
	 Thy/document/pdfsetup.sty Thy/document/session.tex
26738
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    51
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    52
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    53
## clean
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    54
615e1a86787b basic setup for generated document (cf. ../IsarImplementation);
wenzelm
parents:
diff changeset
    55
clean:
26840
ec46381f149d added logic-specific sessions;
wenzelm
parents: 26782
diff changeset
    56
	@rm -f $(LOG)/HOL-IsarRef.gz $(LOG)/HOLCF-IsarRef.gz $(LOG)/ZF-IsarRef.gz