60 |
60 |
61 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy CodeGen/goal1.ML \ |
61 $(LOG)/HOL-CodeGen.gz: $(OUT)/HOL CodeGen/CodeGen.thy CodeGen/goal1.ML \ |
62 CodeGen/goal2.ML CodeGen/simpsplit.ML CodeGen/ROOT.ML |
62 CodeGen/goal2.ML CodeGen/simpsplit.ML CodeGen/ROOT.ML |
63 @$(ISATOOL) usedir $(OUT)/HOL CodeGen |
63 @$(ISATOOL) usedir $(OUT)/HOL CodeGen |
64 |
64 |
|
65 ## HOL-Datatype |
|
66 |
|
67 HOL-Datatype: HOL $(LOG)/HOL-Datatype.gz |
|
68 |
|
69 Datatype/appmap.ML: Datatype/appmap |
|
70 cat Datatype/goal Datatype/appmap Datatype/semi > Datatype/appmap.ML |
|
71 |
|
72 Datatype/ABexp.thy: Datatype/abprolog Datatype/abdata Datatype/abconstseval \ |
|
73 Datatype/abevala Datatype/abevalb Datatype/abconstssubst Datatype/absubsta\ |
|
74 Datatype/absubstb |
|
75 cd Datatype; cat abprolog abdata abconstseval abevala abevalb abconstssubst absubsta absubstb end > ABexp.thy |
|
76 |
|
77 Datatype/Term.thy: Datatype/tprolog Datatype/mutnested Datatype/tdata \ |
|
78 Datatype/tconstssubst Datatype/tsubst Datatype/tsubsts |
|
79 cd Datatype; cat tprolog mutnested tdata tconstssubst tsubst tsubsts end > Term.thy |
|
80 |
|
81 Datatype/Trie.thy: Datatype/trieprolog Datatype/assoc Datatype/trie \ |
|
82 Datatype/triesels Datatype/lookup Datatype/update |
|
83 cd Datatype; cat trieprolog assoc trie triesels lookup update end > Trie.thy |
|
84 |
|
85 $(LOG)/HOL-Datatype.gz: $(OUT)/HOL \ |
|
86 Datatype/ABexp.thy Datatype/Term.thy Datatype/Trie.thy \ |
|
87 Datatype/ROOT.ML Datatype/abgoalind.ML Datatype/autotac.ML \ |
|
88 Datatype/tidproof.ML Datatype/appmap.ML Datatype/lookupempty.ML \ |
|
89 Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML |
|
90 @$(ISATOOL) usedir $(OUT)/HOL Datatype |
65 |
91 |
66 ## HOL-Misc |
92 ## HOL-Misc |
67 |
93 |
68 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
94 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
69 |
95 |