# HG changeset patch
# User wenzelm
# Date 1727380546 -7200
# Node ID cf96b584724df6ff1fa0a2d9b1d13512c8f56db9
# Parent  f74aecc6ef9c386da14c6f07328d955769f4944f
proper 'no_syntax' declarations (amending 8e72f55295fd);

diff -r f74aecc6ef9c -r cf96b584724d src/HOL/Library/Datatype_Records.thy
--- a/src/HOL/Library/Datatype_Records.thy	Thu Sep 26 11:41:51 2024 +0200
+++ b/src/HOL/Library/Datatype_Records.thy	Thu Sep 26 21:55:46 2024 +0200
@@ -30,29 +30,29 @@
   "_constify"           :: "id => ident"                        (\<open>_\<close>)
   "_constify"           :: "longid => ident"                    (\<open>_\<close>)
 
-  "_field_type"         :: "ident => type => field_type"        (\<open>(2_ ::/ _)\<close>)
+  "_field_type"         :: "ident => type => field_type"        (\<open>(\<open>indent=2 notation=\<open>infix field type\<close>\<close>_ ::/ _)\<close>)
   ""                    :: "field_type => field_types"          (\<open>_\<close>)
   "_field_types"        :: "field_type => field_types => field_types"    (\<open>_,/ _\<close>)
-  "_record_type"        :: "field_types => type"                (\<open>(3\<lparr>_\<rparr>)\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
+  "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_\<rparr>)\<close>)
+  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)\<close>)
 
-  "_field"              :: "ident => 'a => field"               (\<open>(2_ =/ _)\<close>)
+  "_field"              :: "ident => 'a => field"               (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>_ =/ _)\<close>)
   ""                    :: "field => fields"                    (\<open>_\<close>)
   "_fields"             :: "field => fields => fields"          (\<open>_,/ _\<close>)
-  "_record"             :: "fields => 'a"                       (\<open>(3\<lparr>_\<rparr>)\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
+  "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_\<rparr>)\<close>)
+  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_,/ (2\<dots> =/ _)\<rparr>)\<close>)
 
-  "_field_update"       :: "ident => 'a => field_update"        (\<open>(2_ :=/ _)\<close>)
+  "_field_update"       :: "ident => 'a => field_update"        (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>_ :=/ _)\<close>)
   ""                    :: "field_update => field_updates"      (\<open>_\<close>)
   "_field_updates"      :: "field_update => field_updates => field_updates"  (\<open>_,/ _\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(3\<lparr>_\<rparr>)\<close> [900, 0] 900)
+  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>\<lparr>_\<rparr>)\<close> [900, 0] 900)
 
 no_syntax (ASCII)
-  "_record_type"        :: "field_types => type"                (\<open>(3'(| _ |'))\<close>)
-  "_record_type_scheme" :: "field_types => type => type"        (\<open>(3'(| _,/ (2... ::/ _) |'))\<close>)
-  "_record"             :: "fields => 'a"                       (\<open>(3'(| _ |'))\<close>)
-  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(3'(| _,/ (2... =/ _) |'))\<close>)
-  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(3'(| _ |'))\<close> [900, 0] 900)
+  "_record_type"        :: "field_types => type"                (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _ |'))\<close>)
+  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _,/ (2... ::/ _) |'))\<close>)
+  "_record"             :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _ |'))\<close>)
+  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>'(| _,/ (2... =/ _) |'))\<close>)
+  "_record_update"      :: "'a => field_updates => 'b"          (\<open>_/(\<open>indent=3 notation=\<open>mixfix record update\<close>\<close>'(| _ |'))\<close> [900, 0] 900)
 
 (* copied and adapted from Record.thy *)