equal
deleted
inserted
replaced
1670 |
1670 |
1671 lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}" |
1671 lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}" |
1672 apply(auto simp add: mem_def) |
1672 apply(auto simp add: mem_def) |
1673 done |
1673 done |
1674 |
1674 |
|
1675 lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)" |
|
1676 apply rule |
|
1677 apply (rule ball_reg_right) |
|
1678 apply auto |
|
1679 done |
1675 |
1680 |
1676 end |
1681 end |