--- a/src/HOL/Record.thy Wed Oct 09 13:06:55 2024 +0200
+++ b/src/HOL/Record.thy Wed Oct 09 13:25:19 2024 +0200
@@ -422,6 +422,9 @@
field_update and
field_updates
+open_bundle record_syntax
+begin
+
syntax
"_constify" :: "id => ident" (\<open>_\<close>)
"_constify" :: "longid => ident" (\<open>_\<close>)
@@ -450,6 +453,8 @@
"_record_scheme" :: "fields => 'a => 'a" (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _,/ (\<open>indent=2 notation=\<open>infix more value\<close>\<close>... =/ _) |'))\<close>)
"_record_update" :: "'a => field_updates => 'b" (\<open>(\<open>open_block notation=\<open>mixfix record update\<close>\<close>_/(3'(| _ |')))\<close> [900, 0] 900)
+end
+
subsection \<open>Record package\<close>