Re: [isabelle] About contradiction method

Glauber Cabral wrote:
I'd like to ask something else that I'm not sure. If I escape a proof of a
theorem/lemma with oops, I cannot use this thm/lemma in the next proofs,
right?Just to be sure, although I know using this without proving it would
not make sense...

Yes. If you want to use the fact, although unproven, you can use the "sorry" method, which proves anything.


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