Re: [isabelle] "Undeclared hyps" in BNF_FP_Def_Sugar

> Theory updates always need to happen within a theory body, as defined by
> Theory.begin_theory ... Theory.end_theory.  Under normal circumstances,
> the system does that for you, so there are not many words in the
> implementation manual what happens outside.  That behaviour is essentially
> undefined (or arbitrary).

Okay, that makes sense.

> There could be more explicit checks and error messages.  I used to have
> that on my TODO list until approx. 15 years ago, and then removed it for
> lack of practical relevance -- at least at that time in the past.

I would find more of these checks very helpful, since in my work I'm often
exercising parts of the system in perhaps unintended ways.


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