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

[Lukas Bulwahn]

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.

Lukas

> Regards,
>
> Mathieu
> _______________________________________________
> isabelle-dev mailing list
> isabelle-dev at in.tum.de
> https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev