[isabelle-dev] NEWS: elimination rules for recursive functions and new command fun_cases

Manuel Eberl eberlm at in.tum.de
Mon Sep 30 11:59:11 CEST 2013

On 30/09/13 11:49, Makarius wrote:
> On Mon, 23 Sep 2013, Manuel Eberl wrote:
>> I sent my changes to Alexander Krauss last Wednesday so that he can
>> review them.
> We are now getting very close to the fork-point for the release.  So
> can you just post the changeset here, or send it to me privately?
>     Makarius

Of course. Here you go.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: fun_cases.ML
Type: text/x-ocaml
Size: 2596 bytes
Desc: not available
URL: <https://mailman46.in.tum.de/pipermail/isabelle-dev/attachments/20130930/76f8347f/attachment-0002.bin>

More information about the isabelle-dev mailing list