# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1658084978 -3600
# Node ID 3ed514e2d93c9ef132a70326e153e6df987100da
# Parent  5af61c89f51ecf2ce151c1bf64d5883fe32a0522
added paper

diff -r 5af61c89f51e -r 3ed514e2d93c Literature/linear-lexer.pdf
Binary file Literature/linear-lexer.pdf has changed
diff -r 5af61c89f51e -r 3ed514e2d93c thys3/src/BlexerSimp.thy
--- a/thys3/src/BlexerSimp.thy	Sun Jul 17 13:07:05 2022 +0100
+++ b/thys3/src/BlexerSimp.thy	Sun Jul 17 20:09:38 2022 +0100
@@ -2,6 +2,15 @@
   imports Blexer 
 begin
 
+
+lemma test:
+  assumes "Q \<Longrightarrow> P"
+  shows "~P \<Longrightarrow> ~Q"
+  using assms
+  apply(erule_tac contrapos_nn)
+  apply(simp)
+  done
+
 fun distinctWith :: "'a list \<Rightarrow> ('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a set \<Rightarrow> 'a list"
   where
   "distinctWith [] eq acc = []"