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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev

Reply via email to