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



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

I see, now the behavior makes perfect sense.

Maybe it would be good to add this sentence to the documentation to help
new users avoid this pitfall?  Apologies if it's already in there and I
missed it.

Thanks,
Christoph





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