doc-src/Tutorial/IsaMakefile
changeset 5850 9712294e60b9
parent 5621 1fe18aca1062
child 6099 d4866f6ff2f9
equal deleted inserted replaced
5849:59d5fe89f787 5850:9712294e60b9
     2 # IsaMakefile for Tutorial
     2 # IsaMakefile for Tutorial
     3 #
     3 #
     4 
     4 
     5 ## targets
     5 ## targets
     6 
     6 
     7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Misc
     7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Misc
     8 
     8 
     9 
     9 
    10 ## global settings
    10 ## global settings
    11 
    11 
    12 SRC = $(ISABELLE_HOME)/src
    12 SRC = $(ISABELLE_HOME)/src
    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