doc-src/Tutorial/IsaMakefile
changeset 6099 d4866f6ff2f9
parent 5850 9712294e60b9
child 9520 73f1c6685367
equal deleted inserted replaced
6098:8648c6651f07 6099:d4866f6ff2f9
     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-Datatype HOL-Misc
     7 default: HOL-ToyList HOL-Ifexpr HOL-CodeGen HOL-Datatype HOL-Recdef HOL-Misc
     8 
     8 
     9 
     9 
    10 ## global settings
    10 ## global settings
    11 
    11 
    12 SRC = $(ISABELLE_HOME)/src
    12 SRC = $(ISABELLE_HOME)/src
    87   Datatype/ROOT.ML Datatype/abgoalind.ML Datatype/autotac.ML \
    87   Datatype/ROOT.ML Datatype/abgoalind.ML Datatype/autotac.ML \
    88   Datatype/tidproof.ML Datatype/appmap.ML Datatype/lookupempty.ML \
    88   Datatype/tidproof.ML Datatype/appmap.ML Datatype/lookupempty.ML \
    89   Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML
    89   Datatype/trieAdds.ML Datatype/triemain.ML Datatype/trieinduct.ML Datatype/trieexhaust.ML
    90 	@$(ISATOOL) usedir $(OUT)/HOL Datatype
    90 	@$(ISATOOL) usedir $(OUT)/HOL Datatype
    91 
    91 
       
    92 ## HOL-Recdef
       
    93 
       
    94 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz
       
    95 
       
    96 Recdef/Examples.thy: Recdef/exprolog Recdef/fib Recdef/sep Recdef/last \
       
    97   Recdef/constsgcd Recdef/gcd Recdef/ack
       
    98 	cd Recdef; cat exprolog fib sep last constsgcd gcd ack end > Examples.thy
       
    99 
       
   100 Recdef/Sep1.thy: Recdef/sep1prolog Recdef/sep1
       
   101 	cd Recdef; cat sep1prolog sep1 end > Sep1.thy
       
   102 
       
   103 Recdef/Sep2.thy: Recdef/sep2prolog Recdef/sep2
       
   104 	cd Recdef; cat sep2prolog sep2 end > Sep2.thy
       
   105 
       
   106 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/ROOT.ML \
       
   107   Recdef/Examples.thy Recdef/Sep1.thy Recdef/Sep2.thy
       
   108 	@$(ISATOOL) usedir $(OUT)/HOL Recdef
       
   109 
    92 ## HOL-Misc
   110 ## HOL-Misc
    93 
   111 
    94 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
   112 HOL-Misc: HOL $(LOG)/HOL-Misc.gz
    95 
   113 
    96 Misc/Tree.thy: Misc/treeprolog Misc/tree Misc/end
   114 Misc/Tree.thy: Misc/treeprolog Misc/tree Misc/end