src/HOL/Record.thy
changeset 61955 e96292f32c3c
parent 61799 4cf66f21b764
child 62117 86a31308a8e1
     1.1 --- a/src/HOL/Record.thy	Mon Dec 28 19:23:15 2015 +0100
     1.2 +++ b/src/HOL/Record.thy	Mon Dec 28 21:47:32 2015 +0100
     1.3 @@ -427,26 +427,26 @@
     1.4    "_field_type"         :: "ident => type => field_type"        ("(2_ ::/ _)")
     1.5    ""                    :: "field_type => field_types"          ("_")
     1.6    "_field_types"        :: "field_type => field_types => field_types"    ("_,/ _")
     1.7 -  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
     1.8 -  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
     1.9 +  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
    1.10 +  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
    1.11  
    1.12    "_field"              :: "ident => 'a => field"               ("(2_ =/ _)")
    1.13    ""                    :: "field => fields"                    ("_")
    1.14    "_fields"             :: "field => fields => fields"          ("_,/ _")
    1.15 -  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
    1.16 -  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
    1.17 +  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
    1.18 +  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    1.19  
    1.20    "_field_update"       :: "ident => 'a => field_update"        ("(2_ :=/ _)")
    1.21    ""                    :: "field_update => field_updates"      ("_")
    1.22    "_field_updates"      :: "field_update => field_updates => field_updates"  ("_,/ _")
    1.23 -  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
    1.24 +  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
    1.25  
    1.26 -syntax (xsymbols)
    1.27 -  "_record_type"        :: "field_types => type"                ("(3\<lparr>_\<rparr>)")
    1.28 -  "_record_type_scheme" :: "field_types => type => type"        ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)")
    1.29 -  "_record"             :: "fields => 'a"                       ("(3\<lparr>_\<rparr>)")
    1.30 -  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)")
    1.31 -  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3\<lparr>_\<rparr>)" [900, 0] 900)
    1.32 +syntax (ASCII)
    1.33 +  "_record_type"        :: "field_types => type"                ("(3'(| _ |'))")
    1.34 +  "_record_type_scheme" :: "field_types => type => type"        ("(3'(| _,/ (2... ::/ _) |'))")
    1.35 +  "_record"             :: "fields => 'a"                       ("(3'(| _ |'))")
    1.36 +  "_record_scheme"      :: "fields => 'a => 'a"                 ("(3'(| _,/ (2... =/ _) |'))")
    1.37 +  "_record_update"      :: "'a => field_updates => 'b"          ("_/(3'(| _ |'))" [900, 0] 900)
    1.38  
    1.39  
    1.40  subsection \<open>Record package\<close>