src/HOL/IsaMakefile
changeset 25171 4a9c25bffc9b
parent 24994 c385c4eabb3b
child 25173 7e1f197a36c5
equal deleted inserted replaced
25170:bd06fd396fd0 25171:4a9c25bffc9b
    35   HOL-NanoJava \
    35   HOL-NanoJava \
    36   HOL-Nominal-Examples \
    36   HOL-Nominal-Examples \
    37   HOL-NumberTheory \
    37   HOL-NumberTheory \
    38   HOL-Prolog \
    38   HOL-Prolog \
    39   HOL-SET-Protocol \
    39   HOL-SET-Protocol \
       
    40   HOL-Statespace \
    40   HOL-Subst \
    41   HOL-Subst \
    41       TLA-Buffer \
    42       TLA-Buffer \
    42       TLA-Inc \
    43       TLA-Inc \
    43       TLA-Memory \
    44       TLA-Memory \
    44   HOL-UNITY \
    45   HOL-UNITY \
   843 $(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word \
   844 $(LOG)/HOL-Word-Examples.gz: $(OUT)/HOL-Word \
   844   Word/Examples/ROOT.ML \
   845   Word/Examples/ROOT.ML \
   845   Word/Examples/WordExamples.thy
   846   Word/Examples/WordExamples.thy
   846 	@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
   847 	@cd Word; $(ISATOOL) usedir $(OUT)/HOL-Word Examples
   847 
   848 
       
   849 ## HOL-Statespace
       
   850 
       
   851 HOL-Statespace: HOL $(LOG)/HOL-Statespace.gz
       
   852 
       
   853 $(LOG)/HOL-Statespace.gz: $(OUT)/HOL Statespace/DistinctTreeProver.thy \
       
   854   Statespace/StateFun.thy Statespace/StateSpaceLocale.thy \
       
   855   Statespace/StateSpaceSyntax.thy StateSpace/StateSpaceEx.thy \
       
   856   Statespace/distinct_tree_prover.ML Statespace/state_space.ML \
       
   857   Statespace/state_fun.ML \
       
   858   Statespace/document/root.tex
       
   859 	@$(ISATOOL) usedir -g true $(OUT)/HOL Statespace
   848 
   860 
   849 ## clean
   861 ## clean
   850 
   862 
   851 clean:
   863 clean:
   852 	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/HOL-Nominal $(OUT)/TLA \
   864 	@rm -f  $(OUT)/HOL $(OUT)/HOL-Complex $(OUT)/HOL-Nominal $(OUT)/TLA \