Skip to content
Snippets Groups Projects
Commit 2e6c28da authored by Balazs Toth's avatar Balazs Toth
Browse files

fix

parent 5f5300a5
No related branches found
No related tags found
No related merge requests found
......@@ -6,8 +6,8 @@
Abstract_Substitution.Natural_Magma_Functor
begin
lemma exists_multiset [intro]: "\<exists>M. x \<in> set_mset M"
by (meson union_single_eq_member)
lemma exists_non_empty_multiset [intro]: "\<exists>M. M \<noteq> {#}"
by (metis empty_not_add_mset)
global_interpretation muliset_magma: natural_magma_with_empty where
to_set = set_mset and plus = "(+)" and wrap = "\<lambda>l. {#l#}" and add = add_mset and empty = "{#}"
......
0% Loading or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment