1
2
(** generic tools **)
3
4
val prems = goalw HOL.thy [Ex_def] "EX x. P x ==> P (@x. P x)";
5
by (resolve_tac prems 1);
6
qed "selectI1";
7
8
goal HOL.thy "(P & Q) = (Q & P)";
9
by (fast_tac prop_cs 1);
10
qed "conj_commut";