changeset 46720 | 9722171731af |
parent 44890 | 22f665a2e91c |
child 58886 | 8a6cac7c7247 |
--- a/src/HOL/MicroJava/DFA/LBVComplete.thy Mon Feb 27 20:42:09 2012 +0100 +++ b/src/HOL/MicroJava/DFA/LBVComplete.thy Mon Feb 27 20:55:30 2012 +0100 @@ -169,7 +169,7 @@ lemma (in lbv) top_le_conv [simp]: "\<top> <=_r x = (x = \<top>)" - by (insert semilat) (simp add: top top_le_conv) + using semilat by (simp add: top) lemma (in lbv) neq_top [simp, elim]: "\<lbrakk> x <=_r y; y \<noteq> \<top> \<rbrakk> \<Longrightarrow> x \<noteq> \<top>"