1.1 --- a/src/HOL/MicroJava/DFA/Listn.thy	Sat Aug 13 12:05:52 2011 +0200
     1.2 +++ b/src/HOL/MicroJava/DFA/Listn.thy	Sat Aug 13 12:23:51 2011 +0200
     1.3 @@ -314,10 +314,6 @@
     1.4  apply (simp add: nth_Cons split: nat.split)
     1.5  done
     1.6  
     1.7 -lemma equals0I_aux:
     1.8 -  "(\<And>y. A y \<Longrightarrow> False) \<Longrightarrow> A = bot_class.bot"
     1.9 -  by (rule equals0I) (auto simp add: mem_def)
    1.10 -
    1.11  lemma acc_le_listI [intro!]:
    1.12    "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
    1.13  apply (unfold acc_def)