Re: [isabelle] Functions in locales cause duplicate fact declaration error



On Wed, 2015-06-03 at 12:27 +0200, Johannes HÃlzl wrote:
> "termination" looks at the last function definition in the current
> context.

FWIW, I stumbled over this before, and I still think it is a
misfeature.

Best,
Tjark






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