[isabelle-dev] The coming release
krauss at in.tum.de
Sat Aug 24 23:27:33 CEST 2013
On 08/17/2013 04:05 PM, Makarius wrote:
> in the past few weeks the coming release has been mentioned in passing
> several times. So far the precise schedule is not clear, but just from
> the distance to Isabelle2013 and the amount of material that is about to
> be finished for Isabelle2013-1, it has to be rather soon after the summer.
> Since Isabelle is a huge and complex system, things that are relevant
> for a release need to be known well in advance.
There is a small extension to the function package pending, which was
written by Manuel Eberl. It produces elimination rules of a new format,
and also provides a "fun_cases" command for ad-hoc elimination that is
analogous to "inductive_cases".
Since there is some user demand for it and it is already functionally
complete, I'd like to integrate this when I am back from vacation in two
weeks, even if there are some minor things to be sorted out.
More information about the isabelle-dev