equal
deleted
inserted
replaced
66 |
66 |
67 subsection {* Prime list and product *} |
67 subsection {* Prime list and product *} |
68 |
68 |
69 lemma prod_append: "prod (xs @ ys) = prod xs * prod ys" |
69 lemma prod_append: "prod (xs @ ys) = prod xs * prod ys" |
70 apply (induct xs) |
70 apply (induct xs) |
71 apply (simp_all add: mult_assoc) |
71 apply (simp_all add: mult.assoc) |
72 done |
72 done |
73 |
73 |
74 lemma prod_xy_prod: |
74 lemma prod_xy_prod: |
75 "prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys" |
75 "prod (x # xs) = prod (y # ys) ==> x * prod xs = y * prod ys" |
76 apply auto |
76 apply auto |