| author | Christian Urban <urbanc@in.tum.de> | 
| Sun, 10 Feb 2019 21:53:57 +0000 | |
| changeset 307 | ee1caac29bb2 | 
| parent 287 | 95b3880d428f | 
| child 330 | 89e6605c4ca4 | 
| permissions | -rw-r--r-- | 
| 
95
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
1  | 
session "Lex" = HOL +  | 
| 
148
 
702ed601349b
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
95 
diff
changeset
 | 
2  | 
theories [document = false]  | 
| 266 | 3  | 
"Spec"  | 
| 
286
 
804fbb227568
added proof for bitcoded algorithm
 
Christian Urban <urbanc@in.tum.de> 
parents: 
280 
diff
changeset
 | 
4  | 
(*"SpecExt"*)  | 
| 266 | 5  | 
"Lexer"  | 
| 
286
 
804fbb227568
added proof for bitcoded algorithm
 
Christian Urban <urbanc@in.tum.de> 
parents: 
280 
diff
changeset
 | 
6  | 
(*"LexerExt"*)  | 
| 
150
 
09f81fee11ce
updated
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents: 
148 
diff
changeset
 | 
7  | 
"Simplifying"  | 
| 287 | 8  | 
"Sulzmann"  | 
| 
248
 
b90ff5abb437
added a proof that Positional ordering is equivalent to direct posix definition
 
Christian Urban <urbanc@in.tum.de> 
parents: 
223 
diff
changeset
 | 
9  | 
"Positions"  | 
| 
286
 
804fbb227568
added proof for bitcoded algorithm
 
Christian Urban <urbanc@in.tum.de> 
parents: 
280 
diff
changeset
 | 
10  | 
(*"PositionsExt"*)  | 
| 259 | 11  | 
"Exercises"  | 
| 
95
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
12  | 
|
| 
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
13  | 
session Paper in "Paper" = Lex +  | 
| 
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
14  | 
options [document = pdf, document_output = "..", document_variants="paper"]  | 
| 
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
15  | 
theories  | 
| 
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
16  | 
"~~/src/HOL/Library/LaTeXsugar"  | 
| 
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
17  | 
"Paper"  | 
| 
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
18  | 
document_files  | 
| 
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
19  | 
"root.bib"  | 
| 
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
20  | 
"root.tex"  | 
| 
 
a33d3040bf7e
started a paper and moved cruft to Attic
 
Christian Urban <christian dot urban at kcl dot ac dot uk> 
parents:  
diff
changeset
 | 
21  | 
|
| 218 | 22  | 
|
23  | 
session Journal in "Journal" = Lex +  | 
|
24  | 
options [document = pdf, document_output = "..", document_variants="journal"]  | 
|
25  | 
theories  | 
|
26  | 
"~~/src/HOL/Library/LaTeXsugar"  | 
|
27  | 
"Paper"  | 
|
| 280 | 28  | 
"PaperExt"  | 
| 218 | 29  | 
document_files  | 
30  | 
"root.bib"  | 
|
31  | 
"root.tex"  |