> On 12 Mar 2016, at 17:30, Roger Bishop Jones <> wrote:
> David,
> This is not an alph-conversion error.
> The reference to apha conversion is a normal qualifier when
> any rule doesn't get what it needs, since in general a statement of of what
> is needed need only be complied with "up to alpha conversion".
> The real problem here (I guess since I can't actually see the command
> which caused the error, and I can't see the error message), is that you
> have not supplied the arguments required by the rule you are using.
> You have to give it a theorem with a disjunction in the conclusion and a 
> theorem
> whose conclusion is the negation of one of the disjuncts.

Yes. David was optimistically expecting q in the conclusion of L3 to hook up 
with ¬ q
in the conclusion of L4, but, as Mark pointed out, you need to use  ¬_¬_intro 
to change
the conclusion of L3 to ¬ ¬ q to get this to work.



Proofpower mailing list

Reply via email to