107 ## ZF-ex |
107 ## ZF-ex |
108 |
108 |
109 ZF-ex: ZF $(LOG)/ZF-ex.gz |
109 ZF-ex: ZF $(LOG)/ZF-ex.gz |
110 |
110 |
111 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \ |
111 $(LOG)/ZF-ex.gz: $(OUT)/ZF ex/Acc.ML ex/Acc.thy ex/BT.ML ex/BT.thy \ |
112 ex/BinEx.ML ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ |
112 ex/BinEx.thy ex/Brouwer.ML ex/Brouwer.thy ex/CoUnit.ML \ |
113 ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Commutation.ML ex/Commutation.thy \ |
113 ex/CoUnit.thy ex/Comb.ML ex/Comb.thy ex/Commutation.ML ex/Commutation.thy \ |
114 ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \ |
114 ex/Data.ML ex/Data.thy ex/Enum.ML ex/Enum.thy \ |
115 ex/LList.ML ex/LList.thy \ |
115 ex/LList.ML ex/LList.thy \ |
116 ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ |
116 ex/Limit.ML ex/Limit.thy ex/ListN.ML ex/ListN.thy ex/Mutil.ML \ |
117 ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ |
117 ex/Mutil.thy ex/Ntree.ML ex/Ntree.thy ex/Primes.ML ex/Primes.thy \ |
118 ex/NatSum.ML ex/NatSum.thy ex/Primrec_defs.ML ex/Primrec_defs.thy \ |
118 ex/NatSum.ML ex/NatSum.thy ex/Primrec_defs.ML ex/Primrec_defs.thy \ |
119 ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ |
119 ex/Primrec.ML ex/Primrec.thy ex/PropLog.ML ex/PropLog.thy ex/ROOT.ML \ |
120 ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ |
120 ex/Ramsey.ML ex/Ramsey.thy ex/Rmap.ML ex/Rmap.thy ex/TF.ML ex/TF.thy \ |
121 ex/Term.ML ex/Term.thy ex/misc.ML |
121 ex/Term.ML ex/Term.thy ex/misc.thy |
122 @$(ISATOOL) usedir $(OUT)/ZF ex |
122 @$(ISATOOL) usedir $(OUT)/ZF ex |
123 |
123 |
124 |
124 |
125 ## clean |
125 ## clean |
126 |
126 |