diff -r 6f20a44c3cb1 -r 881bd98bddee src/HOL/MicroJava/DFA/Kildall.thy
--- a/src/HOL/MicroJava/DFA/Kildall.thy	Thu Aug 20 10:39:26 2020 +0100
+++ b/src/HOL/MicroJava/DFA/Kildall.thy	Fri Aug 21 12:42:57 2020 +0100
@@ -327,10 +327,6 @@
     done
 qed
 
-(*for lex*)
-lemma ne_lesssub_iff [simp]: "y\<noteq>x \<and> x <[r] y \<longleftrightarrow> x <[r] y"
-  by (meson lesssub_def)
-
 lemma iter_properties[rule_format]:
   assumes semilat: "semilat (A, r, f)"
   shows "\<lbrakk> acc r ; pres_type step n A; mono r step n A;