src/HOL/Enum.thy
changeset 61169 4de9ff3ea29a
parent 61076 bdc1e2f0a86a
child 61799 4cf66f21b764
     1.1 --- a/src/HOL/Enum.thy	Sun Sep 13 22:25:21 2015 +0200
     1.2 +++ b/src/HOL/Enum.thy	Sun Sep 13 22:56:52 2015 +0200
     1.3 @@ -446,9 +446,10 @@
     1.4    "enum_ex P = enum_ex (%x. enum_ex (%y. P (x, y)))"
     1.5  
     1.6   
     1.7 -instance by default
     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 +instance
    1.11 +  by standard
    1.12 +    (simp_all add: enum_prod_def distinct_product
    1.13 +      enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
    1.14  
    1.15  end
    1.16