[isabelle-dev] The coming release

[Alexander Krauss]

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.

Alex