tuned;
authorwenzelm
Fri, 11 Oct 2024 10:29:47 +0200
changeset 81148 acd55a0d06f2
parent 81146 87f173836d56
child 81149 0e506128c14a
tuned;
src/Pure/Pure.thy
--- a/src/Pure/Pure.thy	Thu Oct 10 14:13:18 2024 +0200
+++ b/src/Pure/Pure.thy	Fri Oct 11 10:29:47 2024 +0200
@@ -1581,11 +1581,11 @@
 bundle constrain_space_syntax  \<comment> \<open>type constraints with spacing\<close>
 begin
 no_syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_::_\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_::_\<close> [4, 0] 3)
+  "_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic"  (\<open>_::_\<close> [4, 0] 3)
+  "_constrain" :: "prop' \<Rightarrow> type \<Rightarrow> prop'"  (\<open>_::_\<close> [4, 0] 3)
 syntax (output)
-  "_constrain" :: "logic => type => logic"  (\<open>_ :: _\<close> [4, 0] 3)
-  "_constrain" :: "prop' => type => prop'"  (\<open>_ :: _\<close> [4, 0] 3)
+  "_constrain" :: "logic \<Rightarrow> type \<Rightarrow> logic"  (\<open>_ :: _\<close> [4, 0] 3)
+  "_constrain" :: "prop' \<Rightarrow> type \<Rightarrow> prop'"  (\<open>_ :: _\<close> [4, 0] 3)
 end