| changeset 21403 | dd58f13a8eb4 |
| parent 21303 | fa16e4bf8717 |
| child 21601 | 6588b947d631 |
--- a/doc-src/IsarRef/generic.tex Fri Nov 17 02:19:54 2006 +0100 +++ b/doc-src/IsarRef/generic.tex Fri Nov 17 02:19:55 2006 +0100 @@ -29,7 +29,7 @@ ; 'abbreviation' target? mode? (constdecl? prop +) ; - 'notation' target? mode? (nameref mixfix +) + 'notation' target? mode? (nameref mixfix + 'and') ; consts: ((name ('::' type)? structmixfix? | vars) + 'and')