Mercurial Mercurial > hg > lexing / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
corrected typo and corrected proofs in Sulzmann.thy
authorChristian Urban <christian dot urban at kcl dot ac dot uk>
Tue, 05 Apr 2016 14:00:55 +0100
changeset 160 6342d0570502
parent 159 940530087f30
child 161 2778715487a9
corrected typo and corrected proofs in Sulzmann.thy
thys/Paper/Paper.thy file | annotate | diff | comparison | revisions
thys/Sulzmann.thy file | annotate | diff | comparison | revisions
thys/paper.pdf file | annotate | diff | comparison | revisions 
--- a/thys/Paper/Paper.thy	Tue Apr 05 09:27:36 2016 +0100
+++ b/thys/Paper/Paper.thy	Tue Apr 05 14:00:55 2016 +0100
@@ -803,7 +803,7 @@
 
   Derivatives as calculated by \Brz's method are usually more complex
   regular expressions than the initial one; the result is that the
-  deivative-based matching and lexing algorithms are often abysmally slow.
+  derivative-based matching and lexing algorithms are often abysmally slow.
   However, various optimisations are possible, such as the simplifications
   of @{term "ALT ZERO r"}, @{term "ALT r ZERO"}, @{term "SEQ ONE r"} and
   @{term "SEQ r ONE"} to @{term r}. These simplifications can speed up the
--- a/thys/Sulzmann.thy	Tue Apr 05 09:27:36 2016 +0100
+++ b/thys/Sulzmann.thy	Tue Apr 05 14:00:55 2016 +0100
@@ -198,9 +198,6 @@
 apply(simp)
 apply(simp)
 apply(erule Prf_elims)
-apply(simp)
-apply(erule Prf_elims)
-apply(simp)
 apply(auto split: prod.splits)[1]
 oops
 
Binary file thys/paper.pdf has changed
lexing