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-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
smime.p7s
Description: S/MIME Cryptographic Signature
_______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
