Re: [isabelle-dev] not working

2015-04-28 Thread Makarius
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

Re: [isabelle-dev] not working

2015-04-28 Thread 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, L

[isabelle-dev] not working

2015-04-28 Thread 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