--- a/src/ZF/UNITY/MultisetSum.thy Wed Jan 10 15:21:49 2018 +0100
+++ b/src/ZF/UNITY/MultisetSum.thy Wed Jan 10 15:25:09 2018 +0100
@@ -21,12 +21,12 @@
definition
msetsum :: "[i=>i, i, i]=>i" where
- "msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, op +#, g))"
+ "msetsum(g, C, B) == normalize(general_setsum(C, Mult(B), 0, (+#), g))"
definition (* sum for naturals *)
nsetsum :: "[i=>i, i] =>i" where
- "nsetsum(g, C) == general_setsum(C, nat, 0, op #+, g)"
+ "nsetsum(g, C) == general_setsum(C, nat, 0, (#+), g)"
lemma mset_of_normalize: "mset_of(normalize(M)) \<subseteq> mset_of(M)"
@@ -51,7 +51,7 @@
lemma lcomm_mono: "[| C\<subseteq>A; lcomm(A, B, f) |] ==> lcomm(C, B,f)"
by (auto simp add: lcomm_def, blast)
-lemma munion_lcomm [simp]: "lcomm(Mult(A), Mult(A), op +#)"
+lemma munion_lcomm [simp]: "lcomm(Mult(A), Mult(A), (+#))"
by (auto simp add: lcomm_def Mult_iff_multiset munion_lcommute)
(** msetsum **)
@@ -182,4 +182,4 @@
apply (erule Finite_induct, auto)
done
-end
\ No newline at end of file
+end