equal
deleted
inserted
replaced
968 advanced case analysis later. |
968 advanced case analysis later. |
969 |
969 |
970 @{rail \<open> |
970 @{rail \<open> |
971 @@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')') |
971 @@{command case} @{syntax thmdecl}? (name | '(' name (('_' | @{syntax name}) *) ')') |
972 ; |
972 ; |
973 @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) +) ']' ) ? ) +) |
973 @@{attribute case_names} ((@{syntax name} ( '[' (('_' | @{syntax name}) *) ']' ) ? ) +) |
974 ; |
974 ; |
975 @@{attribute case_conclusion} @{syntax name} (@{syntax name} * ) |
975 @@{attribute case_conclusion} @{syntax name} (@{syntax name} * ) |
976 ; |
976 ; |
977 @@{attribute params} ((@{syntax name} * ) + @'and') |
977 @@{attribute params} ((@{syntax name} * ) + @'and') |
978 ; |
978 ; |