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