# HG changeset patch
# User kleing
# Date 1313231031 -7200
# Node ID 9411ed32f3a7ea646ac89c197888b01ac7088340
# Parent  04b3d8327c12350952a048d5d97e952d90d19534
removed unused lemma; removed old-style ;

diff -r 04b3d8327c12 -r 9411ed32f3a7 src/HOL/MicroJava/DFA/Listn.thy
--- a/src/HOL/MicroJava/DFA/Listn.thy	Sat Aug 13 12:05:52 2011 +0200
+++ b/src/HOL/MicroJava/DFA/Listn.thy	Sat Aug 13 12:23:51 2011 +0200
@@ -314,10 +314,6 @@
 apply (simp add: nth_Cons split: nat.split)
 done
 
-lemma equals0I_aux:
-  "(\<And>y. A y \<Longrightarrow> False) \<Longrightarrow> A = bot_class.bot"
-  by (rule equals0I) (auto simp add: mem_def)
-
 lemma acc_le_listI [intro!]:
   "\<lbrakk> order r; acc r \<rbrakk> \<Longrightarrow> acc(Listn.le r)"
 apply (unfold acc_def)