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

Regards,
Jakub Kądziołka




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