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

[Mathieu Giorgino]

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