Mercurial Mercurial > repos > isabelle / diff
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | file | latest | revisions | annotate | diff | comparison | raw | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
src/Doc/Isar_Ref/Spec.thy
changeset 81995 d67dadd69d07
parent 81994 5e50a2b52809 
--- 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
isabelle