lexing: thys/ROOT@c40348a77318 (annotated)

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 fff2e1b40dfc updated Christian Urban <urbanc@in.tum.de> parents: 259 diff changeset	3	"Spec"
286 804fbb227568 added proof for bitcoded algorithm Christian Urban <urbanc@in.tum.de> parents: 280 diff changeset	4	("SpecExt")
266 fff2e1b40dfc updated Christian Urban <urbanc@in.tum.de> parents: 259 diff changeset	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 95b3880d428f updated Christian Urban <urbanc@in.tum.de> parents: 286 diff changeset	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 78dd6bca5627 updated Christian Urban <urbanc@in.tum.de> parents: 257 diff changeset	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 16af5b8bd285 updated Christian Urban <urbanc@in.tum.de> parents: 185 diff changeset	22
330 89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	23	session Journal in "Journal" = HOL +
218 16af5b8bd285 updated Christian Urban <urbanc@in.tum.de> parents: 185 diff changeset	24	options [document = pdf, document_output = "..", document_variants="journal"]
330 89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	25	theories [document = false]
89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	26	"~~/src/HOL/Library/LaTeXsugar"
89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	27	"~~/src/HOL/Library/Sublist"
89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	28	"../Spec"
89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	29	"../RegLangs"
89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	30	"../Lexer"
89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	31	"../Simplifying"
89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	32	"../Sulzmann"
89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	33	"../Positions"
89e6605c4ca4 updated Christian Urban <urbanc@in.tum.de> parents: 287 diff changeset	34	theories [document = true]
218 16af5b8bd285 updated Christian Urban <urbanc@in.tum.de> parents: 185 diff changeset	35	"Paper"
280 c840a99a3e05 updated cu parents: 278 diff changeset	36	"PaperExt"
218 16af5b8bd285 updated Christian Urban <urbanc@in.tum.de> parents: 185 diff changeset	37	document_files
16af5b8bd285 updated Christian Urban <urbanc@in.tum.de> parents: 185 diff changeset	38	"root.bib"
16af5b8bd285 updated Christian Urban <urbanc@in.tum.de> parents: 185 diff changeset	39	"root.tex"

author	Christian Urban <urbanc@in.tum.de>
	Sun, 11 Aug 2019 00:28:14 +0100
changeset 338	c40348a77318
parent 330	89e6605c4ca4
child 362	e51c9a67a68d
permissions	-rw-r--r--