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