equal
deleted
inserted
replaced
184 |
184 |
185 |
185 |
186 section {* Misc. *} |
186 section {* Misc. *} |
187 |
187 |
188 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" |
188 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" |
189 apply (erule make_imp) |
189 apply (erule rev_mp) |
190 apply (induct l) |
190 apply (induct l) |
191 apply simp |
191 apply simp |
192 apply (simp (no_asm)) |
192 apply (simp (no_asm)) |
193 apply auto |
193 apply auto |
194 done |
194 done |