merged

--- a/src/HOL/Enum.thy	Thu Jun 12 17:50:49 2014 +0200
+++ b/src/HOL/Enum.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -447,7 +447,7 @@
 
  
 instance by default
-  (simp_all add: enum_prod_def product_list_set distinct_product
+  (simp_all add: enum_prod_def distinct_product
     enum_UNIV enum_distinct enum_all_prod_def enum_ex_prod_def)
 
 end

--- a/src/HOL/List.thy	Thu Jun 12 17:50:49 2014 +0200
+++ b/src/HOL/List.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -2711,7 +2711,7 @@
 
 subsubsection {* @{const List.product} and @{const product_lists} *}
 
-lemma product_list_set:
+lemma set_product[simp]:
   "set (List.product xs ys) = set xs \<times> set ys"
   by (induct xs) auto
 
@@ -3332,10 +3332,8 @@
 qed (auto simp: dec_def)
 
 lemma distinct_product:
-  assumes "distinct xs" and "distinct ys"
-  shows "distinct (List.product xs ys)"
-  using assms by (induct xs)
-    (auto intro: inj_onI simp add: product_list_set distinct_map)
+  "distinct xs \<Longrightarrow> distinct ys \<Longrightarrow> distinct (List.product xs ys)"
+by (induct xs) (auto intro: inj_onI simp add: distinct_map)
 
 lemma distinct_product_lists:
   assumes "\<forall>xs \<in> set xss. distinct xs"

--- a/src/HOL/String.thy	Thu Jun 12 17:50:49 2014 +0200
+++ b/src/HOL/String.thy	Thu Jun 12 18:47:27 2014 +0200
@@ -224,7 +224,7 @@
 
 instance proof
   show UNIV: "UNIV = set (Enum.enum :: char list)"
-    by (simp add: enum_char_product_enum_nibble UNIV_char product_list_set enum_UNIV)
+    by (simp add: enum_char_product_enum_nibble UNIV_char enum_UNIV)
   show "distinct (Enum.enum :: char list)"
     by (auto intro: inj_onI simp add: enum_char_product_enum_nibble distinct_map distinct_product enum_distinct)
   show "\<And>P. Enum.enum_all P \<longleftrightarrow> Ball (UNIV :: char set) P"