src/HOL/Record.thy
changeset 11489 1fd5469c195e
parent 11473 4546d8d39221
child 11821 ad32c92435db
equal deleted inserted replaced
11488:4ff900551340 11489:1fd5469c195e
    15 nonterminals
    15 nonterminals
    16   ident field_type field_types field fields update updates
    16   ident field_type field_types field fields update updates
    17 
    17 
    18 syntax
    18 syntax
    19   (*field names*)
    19   (*field names*)
    20   "_field_name"         :: "id => ident"                                ("_")
    20   "_constify"           :: "id => ident"                                ("_")
    21   "_field_name"         :: "longid => ident"                            ("_")
    21   "_constify"           :: "longid => ident"                            ("_")
    22 
    22 
    23   (*record types*)
    23   (*record types*)
    24   "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")
    24   "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")
    25   ""                    :: "field_type => field_types"                  ("_")
    25   ""                    :: "field_type => field_types"                  ("_")
    26   "_field_types"        :: "[field_type, field_types] => field_types"   ("_,/ _")
    26   "_field_types"        :: "[field_type, field_types] => field_types"   ("_,/ _")