# HG changeset patch
# User haftmann
# Date 1457467666 -3600
# Node ID 7a9aa69f9b388aadf5f07a8ac84a4500554d9214
# Parent  656e9653c645f676a1688a5985d36e39d4d2a0de
syntax for multiset membership modelled after syntax for set membership

diff -r 656e9653c645 -r 7a9aa69f9b38 NEWS
--- a/NEWS	Mon Mar 07 23:20:11 2016 +0100
+++ b/NEWS	Tue Mar 08 21:07:46 2016 +0100
@@ -54,7 +54,6 @@
 resemble the f.split naming convention, INCOMPATIBILITY.
 
 * Multiset membership is now expressed using set_mset rather than count.
-ASCII infix syntax ":#" has been discontinued.
 
   - Expressions "count M a > 0" and similar simplify to membership
     by default.
diff -r 656e9653c645 -r 7a9aa69f9b38 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Mon Mar 07 23:20:11 2016 +0100
+++ b/src/HOL/Library/Multiset.thy	Tue Mar 08 21:07:46 2016 +0100
@@ -113,11 +113,27 @@
 definition set_mset :: "'a multiset \<Rightarrow> 'a set"
   where "set_mset M = {x. count M x > 0}"
 
-abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<in>#" 50)
-  where "a \<in># M \<equiv> a \<in> set_mset M"
-
-abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"  (infix "\<notin>#" 50)
-  where "a \<notin># M \<equiv> a \<notin> set_mset M"
+abbreviation Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
+  where "Melem a M \<equiv> a \<in> set_mset M"
+
+notation
+  Melem  ("op \<in>#") and
+  Melem  ("(_/ \<in># _)" [51, 51] 50)
+
+notation  (ASCII)
+  Melem  ("op :#") and
+  Melem  ("(_/ :# _)" [51, 51] 50)
+
+abbreviation not_Melem :: "'a \<Rightarrow> 'a multiset \<Rightarrow> bool"
+  where "not_Melem a M \<equiv> a \<notin> set_mset M"
+
+notation
+  not_Melem  ("op \<notin>#") and
+  not_Melem  ("(_/ \<notin># _)" [51, 51] 50)
+
+notation  (ASCII)
+  not_Melem  ("op ~:#") and
+  not_Melem  ("(_/ ~:# _)" [51, 51] 50)
 
 context
 begin
@@ -134,6 +150,10 @@
   "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_\<in>#_./ _)" [0, 0, 10] 10)
   "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_\<in>#_./ _)" [0, 0, 10] 10)
 
+syntax  (ASCII)
+  "_MBall"       :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<forall>_:#_./ _)" [0, 0, 10] 10)
+  "_MBex"        :: "pttrn \<Rightarrow> 'a set \<Rightarrow> bool \<Rightarrow> bool"      ("(3\<exists>_:#_./ _)" [0, 0, 10] 10)
+
 translations
   "\<forall>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Ball A (\<lambda>x. P)"
   "\<exists>x\<in>#A. P" \<rightleftharpoons> "CONST Multiset.Bex A (\<lambda>x. P)"