Re: [isabelle-dev] Towards the release

2016-01-01 Thread Manuel Eberl
I still have a few thousand lines of stuff to merge into the distribution, most notably the definition of the radius of convergence of a series and a number of convergence tests. This would be nice to have in the distribution because two results of mathematical importance rest upon it: the

Re: [isabelle-dev] NEWS: print mode ASCII vs. xsymbols

2016-01-01 Thread Makarius
On Tue, 29 Dec 2015, Makarius wrote: This refers to Isabelle/0a5dd617a88c. A bit more changes may follow later. Here is an updated summary according to Isabelle2016-RC0, with further notes at the bottom: *** General *** * Former "xsymbols" syntax with Isabelle symbols is used by

Re: [isabelle-dev] Towards the release

2016-01-01 Thread Makarius
On Fri, 1 Jan 2016, Lawrence Paulson wrote: I'm still working on a major theorem. It would be nice to include it if possible. Do you have a time estimate for that? Makarius ___ isabelle-dev mailing list isabelle-...@in.tum.de

Re: [isabelle-dev] Towards the release

2016-01-01 Thread Lawrence Paulson
I'm still working on a major theorem. It would be nice to include it if possible. However, I have no major changes on the order of the real vs of_nat rationalisation. Larry > On 1 Jan 2016, at 19:24, Makarius wrote: > > Isabelle2016-RC0 is published, but we are still in