src/HOL/MicroJava/DFA/Kildall.thy

     apply (drule bspec, assumption) 
     apply (drule bspec, assumption)
     apply clarsimp
     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;
      bounded step n; \<forall>p\<in>w0. p < n; ss0 \<in> list n A;