changeset 41229 | d797baa3d57c |
parent 38539 | 3be65f879bcd |
child 42695 | a94ad372b2f5 |
--- a/src/HOL/Record.thy Fri Dec 17 17:08:56 2010 +0100 +++ b/src/HOL/Record.thy Fri Dec 17 17:43:54 2010 +0100 @@ -419,8 +419,15 @@ subsection {* Concrete record syntax *} -nonterminals - ident field_type field_types field fields field_update field_updates +nonterminal + ident and + field_type and + field_types and + field and + fields and + field_update and + field_updates + syntax "_constify" :: "id => ident" ("_") "_constify" :: "longid => ident" ("_")