equal
deleted
inserted
replaced
18 ## Quot |
18 ## Quot |
19 |
19 |
20 Quot: $(LOG)/HOL-Quot.gz |
20 Quot: $(LOG)/HOL-Quot.gz |
21 |
21 |
22 $(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy |
22 $(LOG)/HOL-Quot.gz: Quot/ROOT.ML Quot/*.thy |
23 @$(USEDIR) HOL-Quot Quot |
23 @$(USEDIR) HOL-Nominal Quot |
24 |
24 |
25 paper: $(LOG)/HOL-Quot-Paper.gz |
25 paper: $(LOG)/HOL-Quot-Paper.gz |
26 |
26 |
27 $(LOG)/HOL-Quot-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy |
27 $(LOG)/HOL-Quot-Paper.gz: Paper/ROOT.ML Paper/document/root.tex Paper/*.thy |
28 @$(USEDIR) HOL Paper |
28 @$(USEDIR) HOL Paper |