David,
Your value L7 is a function (type THM -> THM) not a theorem (type THM).
You need to apply it to another theorem to get a new theorem.
]
Regards,
Rob.
On Tue, March 17, 2015 12:59 am, David Topham wrote:
> Thank you so much Rob! That works! If you don't mind another question:
> I
> had g
Ah! Of course! Thank you again! I think I got it now. For completeness
sake, in case anyone else is pursuing this line of learning ProofPower, I
have a link here to the working version with those pieces in place. I do
think there is a lot of potential for using this tool to teach Discrete
Math.
