On 14/08/2016 08:44, David Topham wrote:
Thanks Roger, I am using slides he distributes. He has false
introduction rules starting on page 24 (attached).
Sorry about my poor example, please ignore that since is a confused
use of this technique anyway! -Dave
Looks like he changed the name.
In fact the original name (the one he uses in the book) is good in
¬_elim is available in ProofPower and does what you want (though it is
sligftly more general, it proves anything from a contradiction so you
have to tell it what result you are after).
Details in reference manual.
Proofpower mailing list