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