equal
deleted
inserted
replaced
136 ## HOL-Inductive |
136 ## HOL-Inductive |
137 |
137 |
138 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz |
138 HOL-Inductive: HOL $(LOG)/HOL-Inductive.gz |
139 |
139 |
140 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \ |
140 $(LOG)/HOL-Inductive.gz: $(OUT)/HOL Inductive/ROOT.ML \ |
141 Inductive/Even.thy Inductive/Star.thy Inductive/AB.thy Inductive/Advanced.thy |
141 Inductive/Even.thy Inductive/Mutual.thy Inductive/Star.thy Inductive/AB.thy \ |
|
142 Inductive/Advanced.thy |
142 $(USEDIR) Inductive |
143 $(USEDIR) Inductive |
143 @rm -f tutorial.dvi |
144 @rm -f tutorial.dvi |
144 |
145 |
145 ## HOL-Types |
146 ## HOL-Types |
146 |
147 |