equal
deleted
inserted
replaced
86 |
86 |
87 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz |
87 HOL-Recdef: HOL $(LOG)/HOL-Recdef.gz |
88 |
88 |
89 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \ |
89 $(LOG)/HOL-Recdef.gz: $(OUT)/HOL Recdef/examples.thy Recdef/termination.thy \ |
90 Recdef/simplification.thy Recdef/Induction.thy \ |
90 Recdef/simplification.thy Recdef/Induction.thy \ |
91 Recdef/Nested0.thy Recdef/Nested1.thy |
91 Recdef/Nested0.thy Recdef/Nested1.thy Recdef/Nested2.thy |
92 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef |
92 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Recdef |
93 @rm -f tutorial.dvi |
93 @rm -f tutorial.dvi |
94 |
94 |
95 |
95 |
96 ## HOL-Misc |
96 ## HOL-Misc |