[isabelle-dev] not working

[Larry Paulson]

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="Nat.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