[isabelle-dev] jdk-11

Oracle has released Java 11 last week: it is the new long-term-support (LTS) version for the next 3 years. Public support for Java 8 will stop in Jan-2019. As of Isabelle/9dabb405a3ba we are on that version by default. Due to changes in the licensing and packaging, we are on the official OpenJDK v

Re: [isabelle-dev] Lemma "sum_image_le"

Great, thanks! Alexander Am 06.10.2018 um 13:06 schrieb Tobias Nipkow: > Since Alexander cannot push changes, I have done so now. > > Tobias > > On 28/09/2018 18:44, Lawrence Paulson wrote: >> Sounds good to me! >> Larry >> >>> On 28 Sep 2018, at 14:00, Alexander Maletzky >>> >>

Re: [isabelle-dev] AFP/HLDE

Dear all, > It seems to deliver an executable tool for later use elsewhere, but the > implementation is very fragile. > > We could take it as a model to get such a task right. the situation wrt. generated code is indeed somehow baroque. I am aware of the following layers / approaches: a) Plain

Re: [isabelle-dev] Lemma "sum_image_le"

Since Alexander cannot push changes, I have done so now. Tobias On 28/09/2018 18:44, Lawrence Paulson wrote: Sounds good to me! Larry On 28 Sep 2018, at 14:00, Alexander Maletzky > wrote: lemma "sum_image_le" in theory "Groups_Big", which is stated for