Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] try, try0

view this post on Zulip Email Gateway (Aug 22 2022 at 11:52):

From: Lars Noschinski <noschinl@in.tum.de>
Hi everyone,

I would have expected that try and try0 only work in "prove" mode.
Instead, it suffices when there is a background proof state. I find this
behavior a bit confusing (a student asked me what try is doing in "note
foo try") -- is it intended?

-- Lars

view this post on Zulip Email Gateway (Aug 22 2022 at 11:52):

From: Jasmin Blanchette <jasmin.blanchette@inria.fr>
I don't think so.

Jasmin

Last updated: Nov 21 2024 at 12:39 UTC