equal
deleted
inserted
replaced
152 ## HOL-Types |
152 ## HOL-Types |
153 |
153 |
154 HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz |
154 HOL-Real-Types: HOL-Real $(LOG)/HOL-Real-Types.gz |
155 |
155 |
156 $(LOG)/HOL-Real-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \ |
156 $(LOG)/HOL-Real-Types.gz: $(OUT)/HOL-Real Types/ROOT.ML \ |
157 Types/Numbers.thy Types/Pairs.thy Types/Typedef.thy \ |
157 Types/Numbers.thy Types/Pairs.thy Types/Records.thy Types/Typedef.thy \ |
158 Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \ |
158 Types/Overloading0.thy Types/Overloading1.thy Types/Overloading2.thy \ |
159 Types/Overloading.thy Types/Axioms.thy |
159 Types/Overloading.thy Types/Axioms.thy |
160 $(REALUSEDIR) Types |
160 $(REALUSEDIR) Types |
161 @rm -f tutorial.dvi |
161 @rm -f tutorial.dvi |
162 |
162 |