equal
deleted
inserted
replaced
166 ## HOL-Misc |
166 ## HOL-Misc |
167 |
167 |
168 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
168 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
169 |
169 |
170 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ |
170 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ |
171 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \ |
171 Misc/Plus.thy Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy \ |
172 Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \ |
172 Misc/Option2.thy Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \ |
173 Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy |
173 Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy |
174 $(USEDIR) Misc |
174 $(USEDIR) Misc |
175 @rm -f tutorial.dvi |
175 @rm -f tutorial.dvi |
176 |
176 |
177 |
177 |