[isabelle-dev] not working

[Tobias Nipkow]

That was my mistake. I committed something I did not mean to commit because it 
caused too much nontermination when I tried it with testboard. Thanks for 
alerting me. I have just undone it.

However, HOL-Proofs-ex still fails in the same manner, I have no idea why.

Tobias

On 28/04/2015 17:27, Larry Paulson wrote:
> Today I added some material about complex transcendental functions, and then tested as usual. Two things didn’t work: HOL-Hoare_Parallel and HOL-Proofs-ex. I fixed the former myself. No idea what’s wrong with the latter.
>
> ~/isabelle/Repos/src/HOL: hg id
> bd773c47ad0b tip
>
> Larry
>
>
> val xml =
>     [<5><:><5><:><5><:><5><:><4><:><4>...</4></:><:><:>...</:></:></4></:><:><5><:><5>...</5></:><:><11 0="179192" 1="Nat.arity_type_nat">...</11></:></5></:></5></:><:><11 0="370383" 1="Int.arity_type_int"><:><5><:><0 0="HOL.type_class">...</0></:><:><0 0="Pure.type">...</0></:></5></:><:><:/></:><:><:/><:/><:><0/></:></:></11></:></5></:><:><5><:><5><:><5><:><5>...</5></:><:><5>...</5></:></5></:><:><5><:><5>...</5></:><:><11 0="370601" 1="Int.cr_int_def">...</11></:></5></:></5></:><:><5><:><5><:><5>...</5></:><:><5>...</5></:></5></:><:><5><:><5>...</5></:><:><5>...</5></:></5></:></5></:></5></:></5></:><:><5><:><5><:><5><:><5><:><5>...</5></:><:><5>...</5></:></5></:><:><5><:><5>...</5></:><:><11 0="179192" 1="Nat.arity_type_nat">...</11></:></5></:></5></:><:><5><:><5><:><5>...</5></:><:><5>...</5></:></5></:><:><5><:><5>...</5></:><:><5>...</5></:></5></:></5></:></5></:><:><5><:><5><:><4><:><4>...</4></:><:><:>...</:></:></4></:><:><5><:><5>...</5></:><:><11 0="179192" 1="N
at.arity_type_nat">...</11></:></5></:></5></:><:><5><:><5><:><4>...</4></:><:><5>...</5></:></5></:><:><5><:><5>...</5></:><:><5>...</5></:></5></:></5></:></5></:></5></:></5>]:
>     Encode.body
> val thm =
>     "Abs_Integ ?xa * Abs_Integ ?x =
>      Abs_Integ
>       ((case ?xa of (x, y) => %(u, v). (x * u + y * v, x * v + y * u)) ?x)":
>     thm
> ### theory "XML_Data"
> ### 20.149s elapsed time, 37.337s cpu time, 13.947s GC time
> *** exception Size raised (line 173 of "./basis/LibrarySupport.sml")
> ***
> *** At command "ML_val" (line 59 of "~~/src/HOL/Proofs/ex/XML_Data.thy")
> Unfinished session(s): HOL-Proofs-ex
>
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
>

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5059 bytes
Desc: S/MIME Cryptographic Signature
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20150428/40fb99a9/attachment.bin>