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

Makarius makarius at sketis.net
Thu Mar 12 12:48:36 CET 2015


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


More information about the isabelle-dev mailing list