# HG changeset patch
# User wenzelm
# Date 1028303571 -7200
# Node ID 4cfead92f8f7d9ad33bf9200477192962ca1f056
# Parent  1c3327c348b30c0b57ae059434430f738f887d06
fixed railroads;

diff -r 1c3327c348b3 -r 4cfead92f8f7 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?
   ;