| changeset 7321 | b4dcc32310fb |
| parent 7319 | 3907d597cae6 |
| child 7335 | abba35b98892 |
--- a/doc-src/IsarRef/syntax.tex Mon Aug 23 15:24:00 1999 +0200 +++ b/doc-src/IsarRef/syntax.tex Mon Aug 23 15:27:27 1999 +0200 @@ -134,7 +134,7 @@ \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity} \indexouternonterm{classdecl} \begin{rail} - classdecl: name ('<' (nameref ',' +))? + classdecl: name ('<' (nameref + ','))? ; sort: nameref | lbrace (nameref * ',') rbrace ;