equal
deleted
inserted
replaced
1660 |
1660 |
1661 lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}" |
1661 lemma "(\<lambda> (c::'s \<Rightarrow> bool). \<exists>(x::'s). c = rel x) = {c. \<exists>x. c = rel x}" |
1662 apply(auto simp add: mem_def) |
1662 apply(auto simp add: mem_def) |
1663 done |
1663 done |
1664 |
1664 |
|
1665 lemma ball_reg_right_unfolded: "(\<forall>x. R x \<longrightarrow> P x \<longrightarrow> Q x) \<longrightarrow> (All P \<longrightarrow> Ball R Q)" |
|
1666 apply rule |
|
1667 apply (rule ball_reg_right) |
|
1668 apply auto |
|
1669 done |
1665 |
1670 |
1666 end |
1671 end |