author | kleing |
Sat, 13 Aug 2011 12:23:51 +0200 | |
changeset 44179 | 9411ed32f3a7 |
parent 44178 | 04b3d8327c12 |
child 44180 | a6dc270d3edb |
child 44189 | 4a80017c733f |
--- 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)