# HG changeset patch
# User haftmann
# Date 1275485714 -7200
# Node ID 3464d72326703a43560bf6d56c3cae6bee70f871
# Parent  881fa5012451a26d187b9066c046924b8f9bd934
msetprod_empty, msetprod_singleton

diff -r 881fa5012451 -r 3464d7232670 src/HOL/Number_Theory/UniqueFactorization.thy
--- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 02 15:35:14 2010 +0200
+++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 02 15:35:14 2010 +0200
@@ -72,6 +72,14 @@
 translations
   "PROD i :# A. b" == "CONST msetprod (%i. b) A"
 
+lemma msetprod_empty:
+  "msetprod f {#} = 1"
+  by (simp add: msetprod_def)
+
+lemma msetprod_singleton:
+  "msetprod f {#x#} = f x"
+  by (simp add: msetprod_def)
+
 lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
   apply (simp add: msetprod_def power_add)
   apply (subst setprod_Un2)