src/HOL/Record.thy
changeset 11473 4546d8d39221
parent 10641 d1533f63c738
child 11489 1fd5469c195e
     1.1 --- a/src/HOL/Record.thy	Tue Aug 07 21:27:00 2001 +0200
     1.2 +++ b/src/HOL/Record.thy	Tue Aug 07 22:37:30 2001 +0200
     1.3 @@ -17,8 +17,8 @@
     1.4  
     1.5  syntax
     1.6    (*field names*)
     1.7 -  ""                    :: "id => ident"                                ("_")
     1.8 -  ""                    :: "longid => ident"                            ("_")
     1.9 +  "_field_name"         :: "id => ident"                                ("_")
    1.10 +  "_field_name"         :: "longid => ident"                            ("_")
    1.11  
    1.12    (*record types*)
    1.13    "_field_type"         :: "[ident, type] => field_type"                ("(2_ ::/ _)")