equal
deleted
inserted
replaced
21 |
21 |
22 THY = $(LOG)/HOL-Thy.gz |
22 THY = $(LOG)/HOL-Thy.gz |
23 |
23 |
24 Thy: $(THY) |
24 Thy: $(THY) |
25 |
25 |
26 $(THY): Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML |
26 $(THY): $(OUT)/HOL Thy/ROOT.ML Thy/Setup.thy Thy/Classes.thy ../antiquote_setup.ML ../more_antiquote.ML |
27 @$(USEDIR) HOL Thy |
27 @$(USEDIR) HOL Thy |
28 @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \ |
28 @rm -f Thy/document/isabelle.sty Thy/document/isabellesym.sty \ |
29 Thy/document/pdfsetup.sty Thy/document/session.tex |
29 Thy/document/pdfsetup.sty Thy/document/session.tex |
30 |
30 |
31 |
31 |
32 ## clean |
32 ## clean |
33 |
33 |
34 clean: |
34 clean: |