Re: [isabelle] Isabelle help
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:
This archive was generated by a fusion of
Pipermail (Mailman edition) and