# HG changeset patch
# User wenzelm
# Date 1727992850 -7200
# Node ID 08165a4e105db5f6ca7e2a223b2bafa65600cc9d
# Parent  78fd95fe4a6fec9072446ba5be43899dfbcee2ff
bundles for syntax modifications seen in AFP;

diff -r 78fd95fe4a6f -r 08165a4e105d src/HOL/Set.thy
--- a/src/HOL/Set.thy	Thu Oct 03 23:34:55 2024 +0200
+++ b/src/HOL/Set.thy	Fri Oct 04 00:00:50 2024 +0200
@@ -29,11 +29,23 @@
   not_member  (\<open>'(\<notin>')\<close>) and
   not_member  (\<open>(\<open>notation=\<open>infix \<notin>\<close>\<close>_/ \<notin> _)\<close> [51, 51] 50)
 
+open_bundle member_ASCII_syntax
+begin
 notation (ASCII)
   member  (\<open>'(:')\<close>) and
   member  (\<open>(\<open>notation=\<open>infix :\<close>\<close>_/ : _)\<close> [51, 51] 50) and
   not_member  (\<open>'(~:')\<close>) and
   not_member  (\<open>(\<open>notation=\<open>infix ~:\<close>\<close>_/ ~: _)\<close> [51, 51] 50)
+end
+
+bundle no_member_ASCII_syntax
+begin
+no_notation (ASCII)
+  member  (\<open>'(:')\<close>) and
+  member  (\<open>(\<open>notation=\<open>infix :\<close>\<close>_/ : _)\<close> [51, 51] 50) and
+  not_member  (\<open>'(~:')\<close>) and
+  not_member  (\<open>(\<open>notation=\<open>infix ~:\<close>\<close>_/ ~: _)\<close> [51, 51] 50)
+end
 
 
 text \<open>Set comprehensions\<close>