equal
deleted
inserted
replaced
15 (*Easier to apply than someI if witness ?a comes from an EXformula*) 
15 (*Easier to apply than someI if witness ?a comes from an EXformula*) 
16 Goal "EX x. P x ==> P (SOME x. P x)"; 
16 Goal "EX x. P x ==> P (SOME x. P x)"; 
17 by (etac exE 1); 
17 by (etac exE 1); 
18 by (etac someI 1); 
18 by (etac someI 1); 
19 qed "someI_ex"; 
19 qed "someI_ex"; 
20 AddXEs [someI_ex]; 

21 
20 
22 (*Easier to apply than someI: conclusion has only one occurrence of P*) 
21 (*Easier to apply than someI: conclusion has only one occurrence of P*) 
23 val prems = Goal "[ P a; !!x. P x ==> Q x ] ==> Q (SOME x. P x)"; 
22 val prems = Goal "[ P a; !!x. P x ==> Q x ] ==> Q (SOME x. P x)"; 
24 by (resolve_tac prems 1); 
23 by (resolve_tac prems 1); 
25 by (rtac someI 1); 
24 by (rtac someI 1); 