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
_______________________________________________
isabelle-dev mailing list
isabelle-...@in.tum.de
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
