--- 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 = []"