src/ZF/IsaMakefile
changeset 12186 9b7026a0b0ed
parent 12175 5cf58a1799a7
child 12207 4dff931b852f
equal deleted inserted replaced
12185:54bd9aa3343d 12186:9b7026a0b0ed
   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/Comb.ML Induct/Comb.thy  Induct/FoldSet.ML Induct/FoldSet.thy \
   128   Induct/Binary_Trees.thy Induct/Comb.ML Induct/Comb.thy Induct/Datatypes.thy \
   129   Induct/ListN.ML Induct/ListN.thy \
   129   Induct/FoldSet.ML Induct/FoldSet.thy Induct/ListN.ML Induct/ListN.thy \
   130   Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
   130   Induct/Multiset.ML Induct/Multiset.thy Induct/Mutil.thy \
   131   Induct/Primrec_defs.ML Induct/Primrec_defs.thy \
   131   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/document/root.tex
   134 	@$(ISATOOL) usedir $(OUT)/ZF Induct
   135 	@$(ISATOOL) usedir $(OUT)/ZF Induct
   135 
   136 
   136 
   137 
   137 ## ZF-ex
   138 ## ZF-ex
   138 
   139 
   139 ZF-ex: ZF $(LOG)/ZF-ex.gz
   140 ZF-ex: ZF $(LOG)/ZF-ex.gz
   140 
   141 
   141 $(LOG)/ZF-ex.gz: $(OUT)/ZF  ex/ROOT.ML ex/BT.ML ex/BT.thy \
   142 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/ROOT.ML \
   142   ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
   143   ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \
   143   ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
   144   ex/CoUnit.thy ex/Commutation.ML ex/Commutation.thy \
   144   ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \
       
   145   ex/Limit.ML ex/Limit.thy  ex/LList.ML ex/LList.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\
   146   ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy\
   147   ex/NatSum.ML ex/NatSum.thy \
   147   ex/NatSum.ML ex/NatSum.thy \
   148   ex/Ramsey.ML ex/Ramsey.thy  ex/TF.ML ex/TF.thy \
   148   ex/Ramsey.ML ex/Ramsey.thy  ex/TF.ML ex/TF.thy \
   149   ex/Term.ML ex/Term.thy ex/misc.thy
   149   ex/Term.ML ex/Term.thy ex/misc.thy