# HG changeset patch
# User wenzelm
# Date 1738009862 -3600
# Node ID d67dadd69d072a3d0f8d35a576c2caed993ab7ff
# Parent  5e50a2b5280986e0e4fae43ec3d7bd2272537416
clarified syntax;

diff -r 5e50a2b52809 -r d67dadd69d07 src/Doc/Isar_Ref/Spec.thy
--- a/src/Doc/Isar_Ref/Spec.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/Doc/Isar_Ref/Spec.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -1111,11 +1111,11 @@
   \<^file>\<open>~~/src/HOL/Library/Monad_Syntax.thy\<close>.
 
   \<^rail>\<open>
-    (@@{command adhoc_overloading} | @@{command no_adhoc_overloading})
-      (@{syntax name} (@{syntax term} + ) + @'and')
+    (@@{command adhoc_overloading} | @@{command no_adhoc_overloading}) \<newline>
+      (@{syntax name} ('==' | '\<rightleftharpoons>') (@{syntax term} + ) + @'and')
   \<close>
 
-  \<^descr> @{command "adhoc_overloading"}~\<open>c v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
+  \<^descr> @{command "adhoc_overloading"}~\<open>c \<rightleftharpoons> v\<^sub>1 ... v\<^sub>n\<close> associates variants with an
   existing constant.
 
   \<^descr> @{command "no_adhoc_overloading"} is similar to @{command
diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Examples/Adhoc_Overloading.thy
--- a/src/HOL/Examples/Adhoc_Overloading.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Examples/Adhoc_Overloading.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -35,7 +35,7 @@
 
 text \<open>Which is then overloaded with variants for terms, rules, and TRSs.\<close>
 adhoc_overloading
-  vars term_vars
+  vars \<rightleftharpoons> term_vars
 
 value [nbe] "vars (Fun ''f'' [Var 0, Var 1])"
 
@@ -43,7 +43,7 @@
   "rule_vars (l, r) = vars l \<union> vars r"
 
 adhoc_overloading
-  vars rule_vars
+  vars \<rightleftharpoons> rule_vars
 
 value [nbe] "vars (Var 1, Var 0)"
 
@@ -51,7 +51,7 @@
   "trs_vars R = \<Union>(rule_vars ` R)"
 
 adhoc_overloading
-  vars trs_vars
+  vars \<rightleftharpoons> trs_vars
 
 value [nbe] "vars {(Var 1, Var 0)}"
 
@@ -62,7 +62,7 @@
 
 text \<open>It is also possible to remove variants.\<close>
 no_adhoc_overloading
-  vars term_vars rule_vars 
+  vars \<rightleftharpoons> term_vars rule_vars 
 
 (*value "vars (Var 1)" (*does not have an instance*)*)
 
@@ -71,7 +71,7 @@
 observed by the configuration option \<open>show_variants\<close>.\<close>
 
 adhoc_overloading
-  vars term_vars
+  vars \<rightleftharpoons> term_vars
 
 declare [[show_variants]]
 
@@ -186,7 +186,7 @@
 begin
 
 adhoc_overloading
-  PERMUTE permute
+  PERMUTE \<rightleftharpoons> permute
 
 end
 
@@ -195,7 +195,7 @@
   "permute_atom p a = (Rep_perm p) a"
 
 adhoc_overloading
-  PERMUTE permute_atom
+  PERMUTE \<rightleftharpoons> permute_atom
 
 interpretation atom_permute: permute permute_atom
   by standard (simp_all add: permute_atom_def Rep_perm_simps)
@@ -205,7 +205,7 @@
   "permute_perm p q = p + q - p"
 
 adhoc_overloading
-  PERMUTE permute_perm
+  PERMUTE \<rightleftharpoons> permute_perm
 
 interpretation perm_permute: permute permute_perm
   apply standard
@@ -222,13 +222,13 @@
 begin
 
 adhoc_overloading
-  PERMUTE perm1 perm2
+  PERMUTE \<rightleftharpoons> perm1 perm2
 
 definition permute_fun :: "'a perm \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> ('b \<Rightarrow> 'c)" where
   "permute_fun p f = (\<lambda>x. p \<bullet> (f (-p \<bullet> x)))"
 
 adhoc_overloading
-  PERMUTE permute_fun
+  PERMUTE \<rightleftharpoons> permute_fun
 
 end
 
@@ -244,7 +244,7 @@
   by (unfold_locales)
 
 adhoc_overloading
-  PERMUTE atom_fun_permute.permute_fun
+  PERMUTE \<rightleftharpoons> atom_fun_permute.permute_fun
 
 lemma "(Abs_perm id :: 'a perm) \<bullet> id = id"
   unfolding atom_fun_permute.permute_fun_def
diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -250,7 +250,7 @@
                 | None \<Rightarrow> None)"
 
 adhoc_overloading
-  Monad_Syntax.bind Heap_Monad.bind
+  Monad_Syntax.bind \<rightleftharpoons> Heap_Monad.bind
 
 lemma execute_bind [execute_simps]:
   "execute f h = Some (x, h') \<Longrightarrow> execute (f \<bind> g) h = execute (g x) h'"
diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Library/Monad_Syntax.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -70,6 +70,6 @@
   "(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
 
 adhoc_overloading
-  bind Set.bind Predicate.bind Option.bind List.bind
+  bind \<rightleftharpoons> Set.bind Predicate.bind Option.bind List.bind
 
 end
diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Library/State_Monad.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -89,7 +89,7 @@
   "run_state (bind x f) s = (case run_state x s of (a, s') \<Rightarrow> run_state (f a) s')"
 unfolding bind_def by auto
 
-adhoc_overloading Monad_Syntax.bind bind
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind
 
 lemma bind_left_identity[simp]: "bind (return a) f = f a"
 unfolding return_def bind_def by simp
diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Probability/Giry_Monad.thy
--- a/src/HOL/Probability/Giry_Monad.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Probability/Giry_Monad.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -1092,7 +1092,7 @@
   "bind M f = (if space M = {} then count_space {} else
     join (distr M (subprob_algebra (f (SOME x. x \<in> space M))) f))"
 
-adhoc_overloading Monad_Syntax.bind bind
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind
 
 lemma bind_empty:
   "space M = {} \<Longrightarrow> bind M f = count_space {}"
diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Probability/Probability_Mass_Function.thy
--- a/src/HOL/Probability/Probability_Mass_Function.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Probability/Probability_Mass_Function.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -367,7 +367,7 @@
     done
 qed
 
-adhoc_overloading Monad_Syntax.bind bind_pmf
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind_pmf
 
 lemma ennreal_pmf_bind: "pmf (bind_pmf N f) i = (\<integral>\<^sup>+x. pmf (f x) i \<partial>measure_pmf N)"
   unfolding pmf.rep_eq bind_pmf.rep_eq
diff -r 5e50a2b52809 -r d67dadd69d07 src/HOL/Probability/SPMF.thy
--- a/src/HOL/Probability/SPMF.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/HOL/Probability/SPMF.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -513,7 +513,7 @@
 definition bind_spmf :: "'a spmf \<Rightarrow> ('a \<Rightarrow> 'b spmf) \<Rightarrow> 'b spmf"
   where "bind_spmf x f = bind_pmf x (\<lambda>a. case a of None \<Rightarrow> return_pmf None | Some a' \<Rightarrow> f a')"
 
-adhoc_overloading Monad_Syntax.bind bind_spmf
+adhoc_overloading Monad_Syntax.bind \<rightleftharpoons> bind_spmf
 
 lemma return_None_bind_spmf [simp]: "return_pmf None \<bind> (f :: 'a \<Rightarrow> _) = return_pmf None"
   by(simp add: bind_spmf_def bind_return_pmf)
diff -r 5e50a2b52809 -r d67dadd69d07 src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Mon Jan 27 20:29:02 2025 +0100
+++ b/src/Pure/Pure.thy	Mon Jan 27 21:31:02 2025 +0100
@@ -1422,16 +1422,19 @@
 ML \<open>
 local
 
+val adhoc_overloading_args =
+  Parse.and_list1 ((Parse.const --| (\<^keyword>\<open>\<rightleftharpoons>\<close> || \<^keyword>\<open>==\<close>)) -- Scan.repeat Parse.term);
+
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>adhoc_overloading\<close>
     "add adhoc overloading for constants / fixed variables"
-    (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term)
+    (adhoc_overloading_args
       >> Adhoc_Overloading.adhoc_overloading_cmd true);
 
 val _ =
   Outer_Syntax.local_theory \<^command_keyword>\<open>no_adhoc_overloading\<close>
     "delete adhoc overloading for constants / fixed variables"
-    (Parse.and_list1 (Parse.const -- Scan.repeat Parse.term)
+    (adhoc_overloading_args
       >> Adhoc_Overloading.adhoc_overloading_cmd false);
 
 in end