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 markup, notaly for LaTeX output: treat record fields as quasi-consts;
authorwenzelm
Tue, 07 Jan 2025 21:39:38 +0100
changeset 81742 4b739ed65946
parent 81741 cd28bf530de2
child 81743 fac2045e61d5
more markup, notaly for LaTeX output: treat record fields as quasi-consts;
src/HOL/Record.thy file | annotate | diff | comparison | revisions 
--- a/src/HOL/Record.thy	Tue Jan 07 20:47:42 2025 +0100
+++ b/src/HOL/Record.thy	Tue Jan 07 21:39:38 2025 +0100
@@ -435,13 +435,13 @@
   "_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>_,/ (\<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"              :: "ident => 'a => field"               (\<open>(\<open>indent=2 notation=\<open>infix field value\<close>\<close>(\<open>open_block markup=\<open>const\<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>_,/ (\<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"       :: "ident => 'a => field_update"        (\<open>(\<open>indent=2 notation=\<open>infix field update\<close>\<close>(\<open>open_block markup=\<open>const\<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>(\<open>open_block notation=\<open>mixfix record update\<close>\<close>_/(3\<lparr>_\<rparr>))\<close> [900, 0] 900)
isabelle