doc-src/IsarRef/logics.tex

--- a/doc-src/IsarRef/logics.tex	Fri Aug 02 11:49:55 2002 +0200
+++ b/doc-src/IsarRef/logics.tex	Fri Aug 02 17:52:51 2002 +0200
@@ -100,7 +100,7 @@
   'typedef' altname? abstype '=' repset
   ;
 
-  altname = '(' (name | 'open' name?) ')'
+  altname: '(' (name | 'open' | 'open' name) ')'
   ;
   abstype: typespec infix?
   ;