# HG changeset patch
# User Christian Urban <christian.urban@kcl.ac.uk>
# Date 1658086126 -3600
# Node ID 344a834a093a060cd7dee700a03f5187e911afc7
# Parent  a76458dd9e4c6f9ded81ba395f3c138f1001c1c5
removed junk in BlexerSimp

diff -r a76458dd9e4c -r 344a834a093a thys3/src/BlexerSimp.thy
--- 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 = []"