Nominal/FSet.thy
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