# HG changeset patch
# User wenzelm
# Date 1728475693 -7200
# Node ID affe64a29f566d4cc87dfdc668c09de4134a8c9f
# Parent  52ed95fa465665929d0aefbd51dc5ca9f589a890
more accurate datatype_record_syntax;

diff -r 52ed95fa4656 -r affe64a29f56 src/HOL/Library/Datatype_Records.thy
--- a/src/HOL/Library/Datatype_Records.thy	Wed Oct 09 13:25:19 2024 +0200
+++ b/src/HOL/Library/Datatype_Records.thy	Wed Oct 09 14:08:13 2024 +0200
@@ -35,19 +35,18 @@
   "_constify"               :: "id => ident"                        (\<open>_\<close>)
   "_constify"               :: "longid => ident"                    (\<open>_\<close>)
 
-  "_datatype_field"         :: "ident => 'a => field"               (\<open>(2_ =/ _)\<close>)
+  "_datatype_field"         :: "ident => 'a => field"               (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>_ =/ _)\<close>)
   ""                        :: "field => fields"                    (\<open>_\<close>)
   "_datatype_fields"        :: "field => fields => fields"          (\<open>_,/ _\<close>)
-  "_datatype_record"        :: "fields => 'a"                       (\<open>(3\<lparr>_\<rparr>)\<close>)
-  "_datatype_field_update"  :: "ident => 'a => field_update"        (\<open>(2_ :=/ _)\<close>)
+  "_datatype_record"        :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix datatype record type\<close>\<close>\<lparr>_\<rparr>)\<close>)
+  "_datatype_field_update"  :: "ident => 'a => field_update"        (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>_ :=/ _)\<close>)
   ""                        :: "field_update => field_updates"      (\<open>_\<close>)
   "_datatype_field_updates" :: "field_update => field_updates => field_updates"  (\<open>_,/ _\<close>)
-  "_datatype_record_update" :: "'a => field_updates => 'b"          (\<open>_/(3\<lparr>_\<rparr>)\<close> [900, 0] 900)
+  "_datatype_record_update" :: "'a => field_updates => 'b"          (\<open>(\<open>open_block notation=\<open>mixfix datatype record update\<close>\<close>_/(3\<lparr>_\<rparr>))\<close> [900, 0] 900)
 
 syntax (ASCII)
-  "_datatype_record"        :: "fields => 'a"                       (\<open>(3'(| _ |'))\<close>)
-  "_datatype_record_scheme" :: "fields => 'a => 'a"                 (\<open>(3'(| _,/ (2... =/ _) |'))\<close>)
-  "_datatype_record_update" :: "'a => field_updates => 'b"          (\<open>_/(3'(| _ |'))\<close> [900, 0] 900)
+  "_datatype_record"        :: "fields => 'a"                       (\<open>(\<open>indent=3 notation=\<open>mixfix datatype record type\<close>\<close>'(| _ |'))\<close>)
+  "_datatype_record_update" :: "'a => field_updates => 'b"          (\<open>(\<open>open_block notation=\<open>mixfix datatype record update\<close>\<close>_/(3'(| _ |')))\<close> [900, 0] 900)
 
 end
 
@@ -56,4 +55,4 @@
 ML_file \<open>datatype_records.ML\<close>
 setup \<open>Datatype_Records.setup\<close>
 
-end
\ No newline at end of file
+end