Re: [isabelle] Unfixed variables in "define" command

On Mon Feb 22, 2021 at 1:23 PM CET, Makarius wrote:
> Such "auto fixes" only work for toplevel specification commands, and that is
> already quite delicate and sometimes fragile.

I agree that changing the behavior could be infeasible. However, perhaps
it would be enough to emit a warning message when one uses 'define'
without 'for'?

Jakub Kądziołka

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