changeset 19219 | 8c0b056a18ed |
parent 19072 | 946ef711dc7d |
child 19256 | a49c0f7c9634 |
--- a/doc-src/IsarRef/pure.tex Wed Mar 08 18:00:00 2006 +0100 +++ b/doc-src/IsarRef/pure.tex Wed Mar 08 18:37:24 2006 +0100 @@ -257,7 +257,7 @@ structs: '(' 'structure' (vars + 'and') ')' ; - constdecl: (name '::' type) mixfix | (name '::' type) | name 'where' | mixfix + constdecl: ((name '::' type) mixfix | (name '::' type)) 'where'? | name 'where' ; constdef: thmdecl? prop ;