changeset 2253 | 8954dc5ebd52 |
parent 2250 | c3fd4e42bb4a |
child 2266 | dcffc2f132c9 |
--- a/Nominal/FSet.thy Mon Jun 14 14:28:12 2010 +0200 +++ b/Nominal/FSet.thy Mon Jun 14 14:28:32 2010 +0200 @@ -1672,5 +1672,10 @@ apply(auto simp add: mem_def) done +lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)" +apply rule +apply (rule ball_reg_right) +apply auto +done end