--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/thys3/README.md	Thu Apr 28 15:56:22 2022 +0100
@@ -0,0 +1,26 @@
+# POSIX Lexing with Bitcoded Regular Expressions
+
+Run the code with
+
+```isabelle build -c -v -d . Posix```
+
+Tested with Isabelle2021-1.
+
+
+* RegLangs.thy (contains basic definitions for Regular Languages)
+
+* PosixSpec.thy (contains values and POSIX definitions)
+
+* Positions.thy (shows the equivalence of our POSIX spec and the definition by Okui & Suzuki)
+
+* PDerivs.thy (Partial Derivatives according to Antimirov, size bounds of pderivs)
+
+* Lexer.thy (first algorithm by Sulzmann & Lu without simplification)
+
+* LexerSimp.thy (correctness for simple-minded simplification rules)
+
+* Blexer.thy (second algorithm by Sulzmann & Lu without simplification)
+
+* BlexerSimp.thy (correctness for aggressive simplification rules)
+
+* Finite Bound Result: BasicIdentidies.thy, ClosedForms.thy, GeneralRegexBound, ClosedFormBounds.thy (Section 5 in the paper)
\ No newline at end of file