1.1 --- a/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 02 15:35:14 2010 +0200
     1.2 +++ b/src/HOL/Number_Theory/UniqueFactorization.thy	Wed Jun 02 15:35:14 2010 +0200
     1.3 @@ -72,6 +72,14 @@
     1.4  translations
     1.5    "PROD i :# A. b" == "CONST msetprod (%i. b) A"
     1.6  
     1.7 +lemma msetprod_empty:
     1.8 +  "msetprod f {#} = 1"
     1.9 +  by (simp add: msetprod_def)
    1.10 +
    1.11 +lemma msetprod_singleton:
    1.12 +  "msetprod f {#x#} = f x"
    1.13 +  by (simp add: msetprod_def)
    1.14 +
    1.15  lemma msetprod_Un: "msetprod f (A+B) = msetprod f A * msetprod f B" 
    1.16    apply (simp add: msetprod_def power_add)
    1.17    apply (subst setprod_Un2)