[isabelle-dev] isabelle test failed (HOL-NSA-Examples)

[Andreas Lochbihler]

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, 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
>> user:        Andreas Lochbihler
>> date:        Tue Mar 10 16:35:14 2015 +0100
>> files:       src/HOL/NSA/StarDef.thy
>> description:
>> more type class instances
>>
>>
>> The error message of the NSA "transfer" proof method is a bit obscure.
>>
>>
>>      Makarius
>> _______________________________________________
>> isabelle-dev mailing list
>> isabelle-dev at in.tum.de
>> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev