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