equal
deleted
inserted
replaced
371 |
371 |
372 (*Easier to apply than someI2 if witness ?a comes from an EX-formula*) |
372 (*Easier to apply than someI2 if witness ?a comes from an EX-formula*) |
373 val [major,minor] = Goal "[| EX a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"; |
373 val [major,minor] = Goal "[| EX a. P a; !!x. P x ==> Q x |] ==> Q (Eps P)"; |
374 by (rtac (major RS exE) 1); |
374 by (rtac (major RS exE) 1); |
375 by (etac someI2 1 THEN etac minor 1); |
375 by (etac someI2 1 THEN etac minor 1); |
376 qed "someI2EX"; |
376 qed "someI2_ex"; |
377 |
377 |
378 val prems = Goal |
378 val prems = Goal |
379 "[| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a"; |
379 "[| P a; !!x. P x ==> x=a |] ==> (@x. P x) = a"; |
380 by (rtac someI2 1); |
380 by (rtac someI2 1); |
381 by (REPEAT (ares_tac prems 1)) ; |
381 by (REPEAT (ares_tac prems 1)) ; |