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 _______________________________________________ isabelle-dev mailing list isabelle-...@in.tum.de https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev