Mercurial Mercurial > repos > isabelle / changeset
summary | shortlog | changelog | graph | tags | bookmarks | branches | files | changeset | raw | gz | help
Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
more accurate no_syntax declarations, following ec121999a9cb;
authorwenzelm
Tue, 08 Oct 2024 16:14:36 +0200
changeset 81131 bad7156a7814
parent 81130 7dd81ffaac72
child 81132 dff7dfd8dce3
more accurate no_syntax declarations, following ec121999a9cb;
src/HOL/Library/Datatype_Records.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Library/Datatype_Records.thy	Tue Oct 08 16:13:02 2024 +0200
+++ b/src/HOL/Library/Datatype_Records.thy	Tue Oct 08 16:14:36 2024 +0200
@@ -34,13 +34,13 @@
   ""                    :: "field_type => field_types"          (\<open>_\<close>)
   "_field_types"        :: "field_type => field_types => field_types"    (\<open>_,/ _\<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>)
+  "_record_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>\<lparr>_,/ (\<open>indent=2 notation=\<open>infix more type\<close>\<close>\<dots> ::/ _)\<rparr>)\<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>(\<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>)
+  "_record_scheme"      :: "fields => 'a => 'a"                 (\<open>(\<open>indent=3 notation=\<open>mixfix record value\<close>\<close>\<lparr>_,/ (\<open>indent=2 notation=\<open>infix more value\<close>\<close>\<dots> =/ _)\<rparr>)\<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>)
@@ -49,9 +49,9 @@
 
 no_syntax (ASCII)
   "_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_type_scheme" :: "field_types => type => type"        (\<open>(\<open>indent=3 notation=\<open>mixfix record type\<close>\<close>'(| _,/ (\<open>indent=2 notation=\<open>infix more type\<close>\<close>... ::/ _) |'))\<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_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>indent=3 notation=\<open>mixfix record update\<close>\<close>'(| _ |'))\<close> [900, 0] 900)
 
 (* copied and adapted from Record.thy *)
isabelle