[isabelle-dev] Fwd: [isabelle] list_to_set_comprehension bug ?

[Makarius]

On Thu, 20 Jan 2011, Lukas Bulwahn wrote:

> On 01/19/2011 03:41 PM, Mathieu Giorgino wrote:
>> Hello all,
>>
>> It seems there is a problem with the list_to_set_comprehension tactic for
>> terms containing a pattern matching on a datatype with a single constructor
>> with at least three arguments (It appears as a rather specific problem...).
>>
>>    datatype t = T unit unit unit
>>
>>    (* declare [[ simproc del: list_to_set_comprehension ]] *)
>>
>>    lemma "set (case n of T a b c ⇒ [b]) ≠ {}"
>>      by (auto split:t.splits) (* *** Tactic failed *)
>>
>> Is this a bug ?
>>
>
> It is indeed a bug - Thanks for reporting. I have already fixed it and 
> the patch is on its way into the upcoming release.

See http://isabelle.in.tum.de/repos/isabelle-release/rev/79dae6b7857d


 	Makarius