equal
deleted
inserted
replaced
153 ## HOL-Real-ex |
153 ## HOL-Real-ex |
154 |
154 |
155 HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz |
155 HOL-Real-ex: HOL-Real $(LOG)/HOL-Real-ex.gz |
156 |
156 |
157 $(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML \ |
157 $(LOG)/HOL-Real-ex.gz: $(OUT)/HOL-Real Real/ex/ROOT.ML \ |
158 Real/ex/BinEx.thy |
158 Real/ex/BinEx.thy Real/ex/document/root.tex Real/ex/Sqrt_Irrational.thy |
159 @cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex |
159 @cd Real; $(ISATOOL) usedir $(OUT)/HOL-Real ex |
160 |
160 |
161 |
161 |
162 ## HOL-Real-HahnBanach |
162 ## HOL-Real-HahnBanach |
163 |
163 |