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