--- a/src/Doc/Codegen/Setup.thy Tue Oct 08 23:31:06 2024 +0200
+++ b/src/Doc/Codegen/Setup.thy Wed Oct 09 13:06:55 2024 +0200
@@ -10,13 +10,7 @@
ML_file \<open>../antiquote_setup.ML\<close>
ML_file \<open>../more_antiquote.ML\<close>
-no_syntax (output)
- "_constrain" :: "logic => type => logic" (\<open>_::_\<close> [4, 0] 3)
- "_constrain" :: "prop' => type => 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)
+unbundle constrain_space_syntax
declare [[default_code_width = 74]]
--- a/src/Doc/Tutorial/ToyList/ToyList.thy Tue Oct 08 23:31:06 2024 +0200
+++ b/src/Doc/Tutorial/ToyList/ToyList.thy Wed Oct 09 13:06:55 2024 +0200
@@ -9,7 +9,8 @@
the concrete syntax and name space of theory \<^theory>\<open>Main\<close> as follows.
\<close>
-no_notation Nil ("[]") and Cons (infixr "#" 65) and append (infixr "@" 65)
+unbundle no list_syntax
+no_notation append (infixr "@" 65)
hide_type list
hide_const rev
--- a/src/HOL/Imperative_HOL/Overview.thy Tue Oct 08 23:31:06 2024 +0200
+++ b/src/HOL/Imperative_HOL/Overview.thy Wed Oct 09 13:06:55 2024 +0200
@@ -7,14 +7,7 @@
imports Imperative_HOL "HOL-Library.LaTeXsugar"
begin
-(* type constraints with spacing *)
-no_syntax (output)
- "_constrain" :: "logic => type => logic" (\<open>_::_\<close> [4, 0] 3)
- "_constrain" :: "prop' => type => 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)
+unbundle constrain_space_syntax
(*>*)
text \<open>
--- a/src/HOL/Library/OptionalSugar.thy Tue Oct 08 23:31:06 2024 +0200
+++ b/src/HOL/Library/OptionalSugar.thy Wed Oct 09 13:06:55 2024 +0200
@@ -51,14 +51,7 @@
"_bind (p # CONST DUMMY) e" <= "_bind p (CONST hd e)"
"_bind (CONST DUMMY # p) e" <= "_bind p (CONST tl e)"
-(* type constraints with spacing *)
-no_syntax (output)
- "_constrain" :: "logic => type => logic" (\<open>_::_\<close> [4, 0] 3)
- "_constrain" :: "prop' => type => 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)
+unbundle constrain_space_syntax
(* sorts as intersections *)
--- a/src/Pure/Pure.thy Tue Oct 08 23:31:06 2024 +0200
+++ b/src/Pure/Pure.thy Wed Oct 09 13:06:55 2024 +0200
@@ -1575,6 +1575,20 @@
qed
qed
+
+section \<open>Misc\<close>
+
+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)
+syntax (output)
+ "_constrain" :: "logic => type => logic" (\<open>_ :: _\<close> [4, 0] 3)
+ "_constrain" :: "prop' => type => prop'" (\<open>_ :: _\<close> [4, 0] 3)
+end
+
+
declare [[ML_write_global = false]]
ML_command \<open>\<^assert> (not (can ML_command \<open>() handle _ => ()\<close>))\<close>