--- a/thys3/src/BlexerSimp.thy	Sun Jul 17 20:28:04 2022 +0100
+++ b/thys3/src/BlexerSimp.thy	Sun Jul 17 20:28:46 2022 +0100
@@ -2,15 +2,6 @@
   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 = []"