equal
deleted
inserted
replaced
1 |
1 |
2 context HOL.thy; |
2 context HOL.thy; |
3 |
3 |
4 Goalw [Ex_def] "EX x. P x ==> P (@x. P x)"; |
4 Goalw [Ex_def] "EX x. P x ==> P (@x. P x)"; |
5 ba 1; |
5 by (assume_tac 1); |
6 qed "selectI1"; |
6 qed "selectI1"; |
7 |
7 |
8 context thy; |
8 context thy; |
9 |
9 |
10 |
10 |