# Re: [isabelle] Isabelle help

Hi Rachel,

`Thanks for that. I have created a rule which i am trying to use in the
``proof of theorem 211. The rule is
`

`axiom1b: "(P /<noteq> Q) /<Longrightarrow> ((/<exists> l. (incident P l
``/<and> incident Q l)) /<or> /<not>(/<exists> l. (incident P l /<and>
``incident Q l)))"
`

`Hmm, I don't see what you'd need this axiom for, because it is also an
``instance of the tautology "A \<or> \<not> A". Furthermore, this theorem
``does not unify with the formula of theorem 211 as here P and Q are
``different, while in 211, l and m are different.
`

`However, in general you could use such a theorem with tactics like rule,
``drule, erule, and frule. I guess you are already working (have worked)
``through the examples in the Isabelle/HOL tutorial. If not, see:
`
http://www.cl.cam.ac.uk/research/hvg/Isabelle/dist/Isabelle/doc/tutorial.pdf
best regards,
Simon

*This archive was generated by a fusion of
Pipermail (Mailman edition) and
MHonArc.*