# HG changeset patch
# User nipkow
# Date 1402591636 -7200
# Node ID 8191ccf6a1bd0af5261411022d7a4ae9b489c374
# Parent  b0b9a10e4bf42c88150cf58dcf883cea4f8abf71
added [simp]

diff -r b0b9a10e4bf4 -r 8191ccf6a1bd src/HOL/Enum.thy
--- a/src/HOL/Enum.thy	Thu Jun 12 15:47:36 2014 +0200
+++ b/src/HOL/Enum.thy	Thu Jun 12 18:47:16 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
diff -r b0b9a10e4bf4 -r 8191ccf6a1bd src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Jun 12 15:47:36 2014 +0200
+++ b/src/HOL/List.thy	Thu Jun 12 18:47:16 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"
diff -r b0b9a10e4bf4 -r 8191ccf6a1bd src/HOL/String.thy
--- a/src/HOL/String.thy	Thu Jun 12 15:47:36 2014 +0200
+++ b/src/HOL/String.thy	Thu Jun 12 18:47:16 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"