It should now work again in 034a4d15b52e. Sorry for the trouble.
Andreas
PS: The error message is not so obscure if you look at the types. The left hand side talks
about hyper-naturals, the right hand side about nat.
On 12/03/15 13:56, Andreas Lochbihler wrote:
Hi Makarius,
You are right,
Hi Makarius,
You are right, that's my fault. I'll look into it.
Andreas
On 12/03/15 12:48, Makarius wrote:
On Thu, 12 Mar 2015, Account Isatest wrote:
Unfinished session(s): HOL-NSA-Examples
Presumably this is caused by
changeset: 59676:4762c690a75c
parent: 59654:e327a9ae2d61
On Thu, 12 Mar 2015, Account Isatest wrote:
Unfinished session(s): HOL-NSA-Examples
Presumably this is caused by
changeset: 59676:4762c690a75c
parent: 59654:e327a9ae2d61
user:Andreas Lochbihler
date:Tue Mar 10 16:35:14 2015 +0100
files: src/HOL/NSA/StarDef.thy
