| changeset 24038 | 18182c4aec9e |
| parent 18447 | da548623916a |
| child 24194 | 96013f81faef |
--- a/src/HOL/Bali/Table.thy Sun Jul 29 14:29:51 2007 +0200 +++ b/src/HOL/Bali/Table.thy Sun Jul 29 14:29:52 2007 +0200 @@ -186,7 +186,7 @@ section {* Misc. *} lemma Ball_set_table: "(\<forall> (x,y)\<in> set l. P x y) \<Longrightarrow> \<forall> x. \<forall> y\<in> map_of l x: P x y" -apply (erule make_imp) +apply (erule rev_mp) apply (induct l) apply simp apply (simp (no_asm))