| author | Chengsong |
| Sat, 03 Sep 2022 00:14:20 +0100 | |
| changeset 596 | b306628a0eab |
| parent 563 | c92a41d9c4da |
| child 615 | 8881a09a06fd |
| permissions | -rw-r--r-- |
|
496
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
1 |
session Posix in src = "HOL-Library" + |
|
495
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
2 |
theories[document = false] |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
3 |
"HOL-Library.Sublist" |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
4 |
"RegLangs" |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
5 |
"PosixSpec" |
|
563
c92a41d9c4da
updated paper and theories to include n-times
Christian Urban <christian.urban@kcl.ac.uk>
parents:
496
diff
changeset
|
6 |
(*"Positions"*) |
|
c92a41d9c4da
updated paper and theories to include n-times
Christian Urban <christian.urban@kcl.ac.uk>
parents:
496
diff
changeset
|
7 |
(*"PDerivs"*) |
|
495
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
8 |
"Lexer" |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
9 |
"LexerSimp" |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
10 |
"Blexer" |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
11 |
"BlexerSimp" |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
12 |
"BasicIdentities" |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
13 |
"ClosedForms" |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
14 |
"GeneralRegexBound" |
|
f9cdc295ccf7
a fresh directory with cleaned up code
Christian Urban <christian.urban@kcl.ac.uk>
parents:
diff
changeset
|
15 |
"ClosedFormsBounds" |
|
496
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
16 |
"FBound" |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
17 |
|
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
18 |
|
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
19 |
session Paper = Posix + |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
20 |
options [document_variants="paper", |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
21 |
document = pdf, |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
22 |
document_output = ".", |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
23 |
document_comment_latex, |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
24 |
document_build = "pdflatex", |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
25 |
document_heading_prefix = ""] |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
26 |
theories |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
27 |
Paper |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
28 |
document_files |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
29 |
"root.tex" |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
30 |
"lipics-v2021.cls" |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
31 |
"cc-by.pdf" |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
32 |
"lipics-logo-bw.pdf" |
|
f493a20feeb3
updated to include the paper
Christian Urban <christian.urban@kcl.ac.uk>
parents:
495
diff
changeset
|
33 |
"root.bib" |