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
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
_______________________________________________
isabelle-dev mailing list
[email protected]
https://mailmanbroy.informatik.tu-muenchen.de/mailman/listinfo/isabelle-dev
