Re: [isabelle] Isabelle Foundation & Certification (answer to Makarius)

On 20 Sep 2015, at 14:12, Makarius <makarius at> wrote:
> Users will have true reasons to get worried, when non-trivial changes to core system components and their very foundations can be pushed-in just by making a lot of noise in public.

Quite true. However, we took the decision a long time ago to detect and reject cyclic constant definitions. In this example, a cycle evades detection because it involves a typedef. Closing this loophole would not represent any change in policy. On the other hand, choosing to leave it open would represent a change, and such a change would require justification.


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