[isabelle-dev] NEWS: Computations

Computations generated by the code generator can be embedded directly into ML, alongside with @{code} antiquotations, using the following antiquotations: @{computation … terms: … datatypes: …} : ((term -> term) -> 'ml option -> 'a) -> Proof.context -> term -> 'a @{computation_conv …

[isabelle-dev] The Great Picard Theorem

I have just added this to the Analysis directory, making its inevitable refactoring more necessary. Arguably it should be an AFP entry. Unfortunately, I’m not sufficiently expert in complex analysis to say whether it is core material or not. It looks like a fundamental result to me. We should

Re: [isabelle-dev] Bitbucket SSH craziness escalates

I shall have to file this one under “mercurial mysteries”, which is already a supermassive black hole. I got the push to work, now I’m hoping I don’t have to touch it again for a long time. Larry > On 21 Feb 2017, at 21:56, Blanchette, J.C. wrote: > > >> On

[isabelle-dev] Build failure in slow sessions

Dear developers, there have been some failures in the last two runs of the slow sessions: https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/349/ https://ci.isabelle.systems/jenkins/job/isabelle-nightly-slow/348/ (Relevant changesets are listed there.) Unfortunately there have been