changeset 11489 | 1fd5469c195e |
parent 11473 | 4546d8d39221 |
child 11821 | ad32c92435db |
--- a/src/HOL/Record.thy Wed Aug 08 17:38:29 2001 +0200 +++ b/src/HOL/Record.thy Wed Aug 08 17:38:53 2001 +0200 @@ -17,8 +17,8 @@ syntax (*field names*) - "_field_name" :: "id => ident" ("_") - "_field_name" :: "longid => ident" ("_") + "_constify" :: "id => ident" ("_") + "_constify" :: "longid => ident" ("_") (*record types*) "_field_type" :: "[ident, type] => field_type" ("(2_ ::/ _)")