src/ZF/IsaMakefile
changeset 12229 bfba0eb5124b
parent 12207 4dff931b852f
child 12425 97975229f893
equal deleted inserted replaced
12228:9e5d3c96111a 12229:bfba0eb5124b
   123 ## ZF-Induct
   123 ## ZF-Induct
   124 
   124 
   125 ZF-Induct: ZF $(LOG)/ZF-Induct.gz
   125 ZF-Induct: ZF $(LOG)/ZF-Induct.gz
   126 
   126 
   127 $(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \
   127 $(LOG)/ZF-Induct.gz: $(OUT)/ZF  Induct/ROOT.ML Induct/Acc.ML Induct/Acc.thy \
   128   Induct/Binary_Trees.thy Induct/Comb.ML Induct/Comb.thy Induct/Datatypes.thy \
   128   Induct/Binary_Trees.thy Induct/Brouwer.thy Induct/Comb.ML Induct/Comb.thy \
   129   Induct/FoldSet.ML Induct/FoldSet.thy Induct/ListN.ML Induct/ListN.thy \
   129   Induct/Datatypes.thy Induct/FoldSet.ML Induct/FoldSet.thy Induct/ListN.ML \
   130   Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
   130   Induct/ListN.thy Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
   131   Induct/Primrec_defs.ML Induct/Primrec_defs.thy \
   131   Induct/Ntree.thy Induct/Primrec_defs.ML Induct/Primrec_defs.thy \
   132   Induct/Primrec.ML Induct/Primrec.thy \
   132   Induct/Primrec.ML Induct/Primrec.thy \
   133   Induct/PropLog.ML Induct/PropLog.thy Induct/Rmap.ML Induct/Rmap.thy \
   133   Induct/PropLog.ML Induct/PropLog.thy Induct/Rmap.ML Induct/Rmap.thy \
   134   Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
   134   Induct/Term.thy Induct/Tree_Forest.thy Induct/document/root.tex
   135 	@$(ISATOOL) usedir $(OUT)/ZF Induct
   135 	@$(ISATOOL) usedir $(OUT)/ZF Induct
   136 
   136 
   138 ## ZF-ex
   138 ## ZF-ex
   139 
   139 
   140 ZF-ex: ZF $(LOG)/ZF-ex.gz
   140 ZF-ex: ZF $(LOG)/ZF-ex.gz
   141 
   141 
   142 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML \
   142 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML \
   143   ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
   143   ex/BinEx.thy ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
   144   ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
   144   ex/Limit.ML ex/Limit.thy ex/LList.ML ex/LList.thy ex/Primes.ML ex/Primes.thy \
   145   ex/Limit.ML ex/Limit.thy ex/LList.ML ex/LList.thy \
       
   146   ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \
       
   147   ex/NatSum.ML ex/NatSum.thy ex/Ramsey.ML ex/Ramsey.thy ex/misc.thy
   145   ex/NatSum.ML ex/NatSum.thy ex/Ramsey.ML ex/Ramsey.thy ex/misc.thy
   148 	@$(ISATOOL) usedir $(OUT)/ZF ex
   146 	@$(ISATOOL) usedir $(OUT)/ZF ex
   149 
   147 
   150 
   148 
   151 ## clean
   149 ## clean