Re: [isabelle-dev] NEWS: generated code as proper theory export

2019-02-03 Thread Salomon Sickert
> On 1. Feb 2019, at 15:30, Lars Hupel wrote: > >> What are the remaining uses of these? How much of this can be integrated >> into the formal Isabelle session? How much of it is actually obsolete? > > Hard to tell from a distance, but here's what I gather from reading the > Makefiles: > > – F

Re: [isabelle-dev] Analysis not building

2019-02-03 Thread Bertram Felgenhauer
Florian Haftmann wrote: > > HOL-Analysis can’t be built (reproducibly) with the latest version > > (76f2d492627e). It simply dies, no error message. > > I cannot reproduce this. Neither can I; using polyml-b68438d33c69 I can build HOL-Analysis with Isabelle-24bbc4e30e5b and manual init-component