equal
deleted
inserted
replaced
1 |
1 |
2 |
2 |
3 |
3 |
4 session Journal in Journal = "HOL" + |
4 session Journal in Journal = "HOL" + |
5 options [document_output = "..", document_variants="journal"] |
5 options [ document_output = "..", document_variants="journal", document = pdf] |
6 sessions |
6 sessions |
7 "HOL-Library" |
7 "HOL-Library" |
8 directories |
8 directories |
9 ".." |
9 ".." |
10 theories [document = false] |
10 theories [document = false] |
18 "../Positions" |
18 "../Positions" |
19 theories [document = true] |
19 theories [document = true] |
20 "Paper" |
20 "Paper" |
21 document_files |
21 document_files |
22 "root.bib" |
22 "root.bib" |
23 "root.tex" |
23 "root.tex" |