Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] by fact and try0

Email Gateway (Mar 05 2021 at 12:35):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
Hello,

is there a reason why "try0" does not use the method "fact"?

Stepan

Email Gateway (Mar 09 2021 at 16:38):

From: Jasmin Blanchette via Cl-isabelle-users <cl-isabelle-users@lists.cam.ac.uk>
Dear Stepan,

is there a reason why "try0" does not use the method "fact"?

There's no deep reason, no. I can take note of this, or perhaps somebody wants to implement it before I get to it. It really just would take a couple of lines of code at most I would guess.

Cheers,

Jasmin

Last updated: Jan 04 2025 at 20:18 UTC