| author | Chengsong | 
| Wed, 23 Aug 2023 03:02:31 +0100 | |
| changeset 668 | 3831621d7b14 | 
| parent 642 | 6c13f76c070b | 
| 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"  | 
| 
 
f9cdc295ccf7
a fresh directory with cleaned up code
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
6  | 
"Lexer"  | 
| 
 
f9cdc295ccf7
a fresh directory with cleaned up code
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
7  | 
"LexerSimp"  | 
| 
 
f9cdc295ccf7
a fresh directory with cleaned up code
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
8  | 
"Blexer"  | 
| 
 
f9cdc295ccf7
a fresh directory with cleaned up code
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
9  | 
"BlexerSimp"  | 
| 
 
f9cdc295ccf7
a fresh directory with cleaned up code
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
10  | 
"BasicIdentities"  | 
| 
 
f9cdc295ccf7
a fresh directory with cleaned up code
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
11  | 
"ClosedForms"  | 
| 
 
f9cdc295ccf7
a fresh directory with cleaned up code
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
12  | 
"GeneralRegexBound"  | 
| 
 
f9cdc295ccf7
a fresh directory with cleaned up code
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents:  
diff
changeset
 | 
13  | 
"ClosedFormsBounds"  | 
| 
496
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
14  | 
"FBound"  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
15  | 
|
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
16  | 
|
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
17  | 
session Paper = Posix +  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
18  | 
options [document_variants="paper",  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
19  | 
document = pdf,  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
20  | 
document_output = ".",  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
21  | 
document_comment_latex,  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
22  | 
document_build = "pdflatex",  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
23  | 
document_heading_prefix = ""]  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
24  | 
theories  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
25  | 
Paper  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
26  | 
document_files  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
27  | 
"root.tex"  | 
| 642 | 28  | 
"lipics-v2021.cls"  | 
29  | 
"cc-by.pdf"  | 
|
30  | 
"lipics-logo-bw.pdf"  | 
|
31  | 
"root.bib"  | 
|
32  | 
||
33  | 
||
34  | 
(*  | 
|
35  | 
theories  | 
|
36  | 
Paper  | 
|
37  | 
document_files  | 
|
38  | 
"root.tex"  | 
|
| 
615
 
8881a09a06fd
updated paper for FoSSaCS
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
563 
diff
changeset
 | 
39  | 
"llncs.cls"  | 
| 
496
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
40  | 
"lipics-v2021.cls"  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
41  | 
"cc-by.pdf"  | 
| 
 
f493a20feeb3
updated to include the paper
 
Christian Urban <christian.urban@kcl.ac.uk> 
parents: 
495 
diff
changeset
 | 
42  | 
"lipics-logo-bw.pdf"  | 
| 642 | 43  | 
"root.bib"  | 
44  | 
*)  | 
|
45  |