[isabelle-dev] Towards the next Isabelle release

[Alexander Krauss]

> What are the main pending issues in the pipeline, or projects that still 
> need to be finished?

My list:

Release critical:

- help with proof terms extension

- fix funny warnings in function package pointed out by Brian.


Non-critical:

- integrate decision procedure for nonlinear real arithmetic written by 
Kamil Ciosek (more precisely, by Kamil Ciosek, based on earlier code by 
Amine Chaieb, based on a HOL-Light implementation by Sean McLaughlin and 
John Harrison of a procedure by Hoermander :-))

This is essentially finished, but I want to reduce some code duplication 
before I add it.


Alex