thys3/ROOT
author Chengsong
Mon, 03 Oct 2022 02:08:49 +0100
changeset 609 61139fdddae0
parent 563 c92a41d9c4da
child 615 8881a09a06fd
permissions -rw-r--r--
chap1 totally done
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
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"