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

[Alexander Krauss]

On 09/30/2013 02:41 PM, Makarius wrote:
> On Mon, 30 Sep 2013, Manuel Eberl wrote:
>
>> 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?
>>
>> Of course. Here you go.
>
> Thanks.  This is now Isabelle/d8f7f3d998de.

Thanks for taking care of this.

When looking at the original code earlier, I was also a bit irritated by 
the use of term patterns, but then it got lost somehow.

Nevertheless, it is also a bit irritating that there seems to be no 
proper way of adding support for wildcards to fun_cases (and 
inductive_cases). This should be addressed at some point, but for now we 
are fine.

Alex