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

Mathieu Giorgino mathieu.giorgino at irit.fr
Wed Jan 19 15:41:26 CET 2011

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 ?



More information about the isabelle-dev mailing list