equal
deleted
inserted
replaced
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/*.thy ../antiquote_setup.ML ../more_antiquote.ML |
26 $(THY): Thy/ROOT.ML Thy/*.thy ../antiquote_setup.ML ../more_antiquote.ML |
27 @$(USEDIR) -m no_brackets -m iff HOL Thy |
27 @$(USEDIR) -m no_brackets -m iff HOL-Library 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 |