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