equal
deleted
inserted
replaced
162 |
162 |
163 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
163 HOL-Misc: HOL $(LOG)/HOL-Misc.gz |
164 |
164 |
165 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ |
165 $(LOG)/HOL-Misc.gz: $(OUT)/HOL Misc/ROOT.ML Misc/Tree.thy Misc/Tree2.thy \ |
166 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \ |
166 Misc/fakenat.thy Misc/natsum.thy Misc/pairs.thy Misc/Option2.thy \ |
167 Misc/types.thy Misc/prime_def.thy Misc/case_exprs.thy \ |
167 Misc/types.thy Misc/prime_def.thy Misc/Translations.thy Misc/case_exprs.thy \ |
168 Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy |
168 Misc/simp.thy Misc/Itrev.thy Misc/AdvancedInd.thy Misc/appendix.thy |
169 $(USEDIR) Misc |
169 $(USEDIR) Misc |
170 @rm -f tutorial.dvi |
170 @rm -f tutorial.dvi |
171 |
171 |
172 |
172 |