Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)
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-...@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 ___ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)
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
Re: [isabelle-dev] isabelle test failed (HOL-NSA-Examples)
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
