equal
deleted
inserted
replaced
1 (* Title: HOL/Record.thy |
1 (* Title: HOL/Record.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen |
3 Author: Wolfgang Naraschewski, Norbert Schirmer and Markus Wenzel, TU Muenchen |
4 *) |
4 *) |
5 |
5 |
6 theory Record |
6 theory Record |
7 imports Product_Type |
7 imports Product_Type |
8 files ("Tools/record_package.ML") |
8 files ("Tools/record_package.ML") |
56 "_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
56 "_record_type_scheme" :: "[field_types, type] => type" ("(3\<lparr>_,/ (2\<dots> ::/ _)\<rparr>)") |
57 "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
57 "_record" :: "fields => 'a" ("(3\<lparr>_\<rparr>)") |
58 "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
58 "_record_scheme" :: "[fields, 'a] => 'a" ("(3\<lparr>_,/ (2\<dots> =/ _)\<rparr>)") |
59 "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
59 "_record_update" :: "['a, updates] => 'b" ("_/(3\<lparr>_\<rparr>)" [900,0] 900) |
60 |
60 |
61 use "Tools/record_package.ML"; |
61 use "Tools/record_package.ML" |
62 setup RecordPackage.setup; |
62 setup RecordPackage.setup |
63 |
63 |
64 end |
64 end |
65 |
65 |