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

[Andreas Lochbihler]

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