54 "_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
54 "_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
55 "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
55 "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
56 "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
56 "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
57 "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
57 "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
58 |
58 |
59 (* |
|
60 |
|
61 "_structure" :: "fields => 'a" ("(3{| _ |})") |
|
62 "_structure_scheme" :: "[fields, 'a] => 'a" ("(3{| _,/ (2... =/ _) |})") |
|
63 |
|
64 "_structure_update_name":: idt |
|
65 "_structure_update" :: "['a, updates] \<Rightarrow> 'b" ("_/(3{| _ |})" [900,0] 900) |
|
66 |
|
67 "_structure_type" :: "field_types => type" ("(3{| _ |})") |
|
68 "_structure_type_scheme" :: "[field_types, type] => type" |
|
69 ("(3{| _,/ (2... ::/ _) |})") |
|
70 syntax (xsymbols) |
|
71 |
|
72 "_structure_scheme" :: "[fields, 'a] => 'a" ("(3{|_,/ (2\<dots> =/ _)|})") |
|
73 |
|
74 "_structure_type_scheme" :: "[field_types, type] => type" |
|
75 ("(3{|_,/ (2\<dots> ::/ _)|})") |
|
76 |
|
77 *) |
|
78 use "Tools/record_package.ML"; |
59 use "Tools/record_package.ML"; |
79 setup RecordPackage.setup; |
60 setup RecordPackage.setup; |
80 |
61 |
81 end |
62 end |
82 |
63 |