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
ProofPower.
¬_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.
Roger
_______________________________________________
Proofpower mailing list
Proofpower@lemma-one.com
http://lemma-one.com/mailman/listinfo/proofpower_lemma-one.com
