equal
deleted
inserted
replaced
1 session "Lex" = HOL + |
1 session "Lex" = HOL + |
2 theories [document = false] |
2 theories [document = false] |
3 "Lexer" |
3 "Lexer" |
4 "LexerExt" |
4 "LexerExt" |
5 "Simplifying" |
5 "Simplifying" |
6 "Sulzmann" |
6 (*"Sulzmann"*) |
7 |
7 "Positions" |
8 |
8 |
9 session Paper in "Paper" = Lex + |
9 session Paper in "Paper" = Lex + |
10 options [document = pdf, document_output = "..", document_variants="paper"] |
10 options [document = pdf, document_output = "..", document_variants="paper"] |
11 theories |
11 theories |
12 "~~/src/HOL/Library/LaTeXsugar" |
12 "~~/src/HOL/Library/LaTeXsugar" |