equal
deleted
inserted
replaced
132 ## HOL-Inductive |
132 ## HOL-Inductive |
133 |
133 |
134 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz |
134 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz |
135 |
135 |
136 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \ |
136 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \ |
137 Inductive/Even.thy Inductive/Star.thy Inductive/AB.thy Inductive/Acc.thy |
137 Inductive/Even.thy Inductive/Star.thy Inductive/AB.thy Inductive/Advanced.thy |
138 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive |
138 @$(ISATOOL) usedir -i true -d dvi -D document $(OUT)/HOL Inductive |
139 @rm -f tutorial.dvi |
139 @rm -f tutorial.dvi |
140 |
140 |
141 ## HOL-Types |
141 ## HOL-Types |
142 |
142 |