| changeset 321 | e450fa467e3f |
| parent 320 | 185921021551 |
| 320:185921021551 | 321:e450fa467e3f |
|---|---|
19 |
19 |
20 ## Command |
20 ## Command |
21 |
21 |
22 Command: $(LOG)/HOL-Command.gz |
22 Command: $(LOG)/HOL-Command.gz |
23 |
23 |
24 $(LOG)/HOL-Command.gz: ## Command/ROOT.ML Command/document/root.tex Command/*.thy |
24 $(LOG)/HOL-Command.gz: Command/ROOT.ML Command/*.thy |
25 @$(USEDIR) HOL Command |
25 @$(USEDIR) HOL Command |
26 |
26 |
27 |
27 |
28 ## clean |
28 ## clean |
29 |
29 |