Re: [isabelle] try, try0

> 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?

I don't think so.


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