[isabelle-dev] Towards the next Isabelle release
krauss at in.tum.de
Fri May 7 10:49:09 CEST 2010
> What are the main pending issues in the pipeline, or projects that still
> need to be finished?
- help with proof terms extension
- fix funny warnings in function package pointed out by Brian.
- 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.
More information about the isabelle-dev