equal
deleted
inserted
replaced
19 |
19 |
20 ## Sugar |
20 ## Sugar |
21 |
21 |
22 Sugar: $(LOG)/HOL-Sugar.gz |
22 Sugar: $(LOG)/HOL-Sugar.gz |
23 |
23 |
24 $(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/document/root.tex Sugar/document/root.bib \ |
24 $(LOG)/HOL-Sugar.gz: Sugar/ROOT.ML Sugar/Sugar.thy \ |
25 ../../HOL/Library/LaTeXsugar.thy ../../HOL/Library/OptinalSugar.thy |
25 Sugar/document/root.tex Sugar/document/root.bib \ |
|
26 ../../HOL/Library/LaTeXsugar.thy ../../HOL/Library/OptionalSugar.thy |
26 @$(USEDIR) HOL Sugar |
27 @$(USEDIR) HOL Sugar |
27 |
28 |
28 |
29 |
29 ## clean |
30 ## clean |
30 |
31 |