doc-src/Tutorial/IsaMakefile
author wenzelm
Fri, 16 Jul 1999 22:24:42 +0200
changeset 7024 44bd3c094fd6
parent 6099 d4866f6ff2f9
child 9520 73f1c6685367
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
5621
1fe18aca1062 runs test
nipkow
parents:
diff changeset
     1
#
1fe18aca1062 runs test
nipkow
parents:
diff changeset
     2
# IsaMakefile for Tutorial
1fe18aca1062 runs test
nipkow
parents:
diff changeset
     3
#
1fe18aca1062 runs test
nipkow
parents:
diff changeset
     4
1fe18aca1062 runs test
nipkow
parents:
diff changeset
     5
## targets
1fe18aca1062 runs test
nipkow
parents:
diff changeset
     6
6099
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
     7
default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Recdef HOL-Misc
5621
1fe18aca1062 runs test
nipkow
parents:
diff changeset
     8
1fe18aca1062 runs test
nipkow
parents:
diff changeset
     9
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    10
## global settings
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    11
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    12
SRC = $(ISABELLE_HOME)/src
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    13
OUT = $(ISABELLE_OUTPUT)
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    14
LOG = $(OUT)/log
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    15
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    16
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    17
## HOL
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    18
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    19
HOL:
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    20
	@cd $(SRC)/HOL; $(ISATOOL) make HOL
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    21
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    22
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    23
## HOL-Ifexpr
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    24
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    25
HOL-Ifexpr: HOL $(LOG)/HOL-Ifexpr.gz
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    26
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    27
Ifexpr/Ifexpr.thy: Ifexpr/prolog Ifexpr/boolex Ifexpr/value Ifexpr/ifex \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    28
  Ifexpr/valif Ifexpr/bool2if Ifexpr/normif Ifexpr/norm Ifexpr/normal \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    29
  Ifexpr/end
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    30
	@cd Ifexpr; \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    31
	cat prolog boolex value ifex valif bool2if normif norm normal \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    32
	  end > Ifexpr.thy
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    33
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    34
$(LOG)/HOL-Ifexpr.gz: $(OUT)/HOL Ifexpr/Ifexpr.thy Ifexpr/ROOT.ML
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    35
	@$(ISATOOL) usedir $(OUT)/HOL Ifexpr
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    36
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    37
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    38
## HOL-ToyList
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    39
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    40
HOL-ToyList: HOL $(LOG)/HOL-ToyList.gz
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    41
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    42
ToyList/ToyList.ML: ToyList/autotac ToyList/addsimps2 ToyList/inductxs \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    43
  ToyList/lemma1 ToyList/lemma2 ToyList/lemma3 \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    44
  ToyList/qed1 ToyList/qed2 ToyList/qed3 ToyList/thm ToyList/qed
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    45
	cd ToyList; \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    46
	cat lemma2 inductxs autotac qed2 addsimps2 lemma3 qed3 \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    47
	    lemma1 inductxs autotac qed1 thm inductxs autotac qed > ToyList.ML
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    48
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    49
$(LOG)/HOL-ToyList.gz: $(OUT)/HOL ToyList/ToyList.thy ToyList/ToyList.ML \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    50
  ToyList/ROOT.ML
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    51
	@$(ISATOOL) usedir $(OUT)/HOL ToyList
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    52
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    53
## HOL-CodeGen
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    54
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    55
HOL-CodeGen: HOL $(LOG)/HOL-CodeGen.gz
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    56
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    57
CodeGen/CodeGen.thy: CodeGen/prolog CodeGen/expr CodeGen/value \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    58
  CodeGen/instr CodeGen/exec CodeGen/comp CodeGen/end
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    59
	cd CodeGen; cat prolog expr value instr exec comp end > CodeGen.thy
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    60
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    61
$(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy CodeGen/goal1.ML \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    62
  CodeGen/goal2.ML CodeGen/simpsplit.ML CodeGen/ROOT.ML
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    63
	@$(ISATOOL) usedir $(OUT)/HOL CodeGen
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    64
5850
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    65
## HOL-Datatype
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    66
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    67
HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    68
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    69
Datatype/appmap.ML: Datatype/appmap
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    70
	cat Datatype/goal Datatype/appmap Datatype/semi > Datatype/appmap.ML
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    71
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    72
Datatype/ABexp.thy: Datatype/abprolog Datatype/abdata Datatype/abconstseval \
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    73
  Datatype/abevala Datatype/abevalb Datatype/abconstssubst Datatype/absubsta\
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    74
  Datatype/absubstb
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    75
	cd Datatype; cat abprolog abdata abconstseval abevala abevalb abconstssubst absubsta absubstb end > ABexp.thy
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    76
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    77
Datatype/Term.thy: Datatype/tprolog Datatype/mutnested Datatype/tdata \
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    78
  Datatype/tconstssubst Datatype/tsubst Datatype/tsubsts
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    79
	cd Datatype; cat tprolog mutnested tdata tconstssubst tsubst tsubsts end > Term.thy
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    80
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    81
Datatype/Trie.thy: Datatype/trieprolog Datatype/assoc Datatype/trie \
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    82
  Datatype/triesels Datatype/lookup Datatype/update
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    83
	cd Datatype; cat trieprolog assoc trie triesels lookup update end > Trie.thy
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    84
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    85
$(LOG)/HOL-Datatype.gz: $(OUT)/HOL \
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    86
  Datatype/ABexp.thy Datatype/Term.thy Datatype/Trie.thy \
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    87
  Datatype/ROOT.ML Datatype/abgoalind.ML Datatype/autotac.ML \
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    88
  Datatype/tidproof.ML Datatype/appmap.ML Datatype/lookupempty.ML \
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    89
  Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML
9712294e60b9 *** empty log message ***
nipkow
parents: 5621
diff changeset
    90
	@$(ISATOOL) usedir $(OUT)/HOL Datatype
5621
1fe18aca1062 runs test
nipkow
parents:
diff changeset
    91
6099
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
    92
## HOL-Recdef
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
    93
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
    94
HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
    95
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
    96
Recdef/Examples.thy: Recdef/exprolog Recdef/fib Recdef/sep Recdef/last \
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
    97
  Recdef/constsgcd Recdef/gcd Recdef/ack
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
    98
	cd Recdef; cat exprolog fib sep last constsgcd gcd ack end > Examples.thy
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
    99
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   100
Recdef/Sep1.thy: Recdef/sep1prolog Recdef/sep1
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   101
	cd Recdef; cat sep1prolog sep1 end > Sep1.thy
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   102
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   103
Recdef/Sep2.thy: Recdef/sep2prolog Recdef/sep2
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   104
	cd Recdef; cat sep2prolog sep2 end > Sep2.thy
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   105
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   106
$(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML \
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   107
  Recdef/Examples.thy Recdef/Sep1.thy Recdef/Sep2.thy
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   108
	@$(ISATOOL) usedir $(OUT)/HOL Recdef
d4866f6ff2f9 verbatim
nipkow
parents: 5850
diff changeset
   109
5621
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   110
## HOL-Misc
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   111
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   112
HOL-Misc: HOL $(LOG)/HOL-Misc.gz
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   113
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   114
Misc/Tree.thy: Misc/treeprolog Misc/tree Misc/end
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   115
	cd Misc; cat treeprolog tree end > Tree.thy
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   116
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   117
Misc/NatSum.thy: Misc/natsumprolog Misc/natsum Misc/end
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   118
	cd Misc; cat natsumprolog natsum end > NatSum.thy
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   119
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   120
Misc/Types.thy: Misc/typesprolog Misc/types Misc/end
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   121
	cd Misc; cat typesprolog types end > Types.thy
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   122
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   123
Misc/Defs.thy: Misc/defsprolog Misc/consts Misc/defs Misc/end
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   124
	cd Misc; cat defsprolog consts defs end > Defs.thy
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   125
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   126
Misc/ConstDefs.thy: Misc/constdefsprolog Misc/constdefs Misc/end
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   127
	cd Misc; cat constdefsprolog constdefs end > ConstDefs.thy
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   128
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   129
$(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/exhaust.ML Misc/autotac.ML \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   130
  Misc/Tree.thy Misc/NatSum.thy Misc/NatSum.ML Misc/Types.thy \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   131
  Misc/Defs.thy Misc/ConstDefs.thy \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   132
  Misc/Exor.thy Misc/exorgoal.ML Misc/exorproof.ML \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   133
  Misc/splitif.ML Misc/splitlist.ML Misc/induct_auto.ML \
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   134
  Misc/Itrev.thy Misc/itrev1.ML Misc/itrev2.ML Misc/itrev3.ML
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   135
	@$(ISATOOL) usedir $(OUT)/HOL Misc
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   136
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   137
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   138
## clean
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   139
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   140
clean:
1fe18aca1062 runs test
nipkow
parents:
diff changeset
   141
	@rm -f $(LOG)/HOL-Ifexpr.gz $(LOG)/HOL-Misc.gz