[isabelle] try, try0



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




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