On Tue, 28 Apr 2015, 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.
I am presently not on the isa
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, L
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