src/HOL/Enum.thy
changeset 57247 8191ccf6a1bd
parent 55088 57c82e01022b
child 57818 51aa30c9ee4e
     1.1 --- a/src/HOL/Enum.thy	Thu Jun 12 15:47:36 2014 +0200
     1.2 +++ b/src/HOL/Enum.thy	Thu Jun 12 18:47:16 2014 +0200
     1.3 @@ -447,7 +447,7 @@
     1.4  
     1.5   
     1.6  instance by default
     1.7 -  (simp_all add: enum_prod_def product_list_set distinct_product
     1.8 +  (simp_all add: enum_prod_def distinct_product
     1.9      enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
    1.10  
    1.11  end