changeset 1899 | 0075a8d26a80 |
parent 1440 | de6f18da81bb |
1898:260a9711f507 | 1899:0075a8d26a80 |
---|---|
4 val prems = goalw HOL.thy [Ex_def] "EX x. P x ==> P (@x. P x)"; |
4 val prems = goalw HOL.thy [Ex_def] "EX x. P x ==> P (@x. P x)"; |
5 by (resolve_tac prems 1); |
5 by (resolve_tac prems 1); |
6 qed "selectI1"; |
6 qed "selectI1"; |
7 |
7 |
8 goal HOL.thy "(P & Q) = (Q & P)"; |
8 goal HOL.thy "(P & Q) = (Q & P)"; |
9 by (fast_tac prop_cs 1); |
9 by (Fast_tac 1); |
10 qed "conj_commut"; |
10 qed "conj_commut"; |