1.1 --- a/doc-src/IsarRef/logics.tex	Tue Feb 12 20:32:23 2002 +0100
     1.2 +++ b/doc-src/IsarRef/logics.tex	Tue Feb 12 20:33:03 2002 +0100
     1.3 @@ -90,9 +90,9 @@
     1.4  \end{matharray}
     1.5  
     1.6  \begin{rail}
     1.7 -  'typedecl' typespec infix? comment?
     1.8 +  'typedecl' typespec infix?
     1.9    ;
    1.10 -  'typedef' parname? typespec infix? \\ '=' term comment?
    1.11 +  'typedef' parname? typespec infix? '=' term
    1.12    ;
    1.13  \end{rail}
    1.14  
    1.15 @@ -186,7 +186,7 @@
    1.16  
    1.17    dtspec: parname? typespec infix? '=' (cons + '|')
    1.18    ;
    1.19 -  cons: name (type * ) mixfix? comment?
    1.20 +  cons: name (type * ) mixfix?
    1.21    ;
    1.22    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    1.23  \end{rail}
    1.24 @@ -236,14 +236,12 @@
    1.25  \begin{rail}
    1.26    'primrec' parname? (equation + )
    1.27    ;
    1.28 -  'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
    1.29 +  'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
    1.30    ;
    1.31 -  recdeftc thmdecl? tc comment?
    1.32 +  recdeftc thmdecl? tc
    1.33    ;
    1.34  
    1.35 -  equation: thmdecl? eqn
    1.36 -  ;
    1.37 -  eqn: prop comment?
    1.38 +  equation: thmdecl? prop
    1.39    ;
    1.40    hints: '(' 'hints' (recdefmod * ) ')'
    1.41    ;
    1.42 @@ -329,11 +327,11 @@
    1.43    'mono' (() | 'add' | 'del')
    1.44    ;
    1.45  
    1.46 -  sets: (term comment? +)
    1.47 +  sets: (term +)
    1.48    ;
    1.49 -  intros: 'intros' (thmdecl? prop comment? +)
    1.50 +  intros: 'intros' (thmdecl? prop +)
    1.51    ;
    1.52 -  monos: 'monos' thmrefs comment?
    1.53 +  monos: 'monos' thmrefs
    1.54    ;
    1.55  \end{rail}
    1.56  
    1.57 @@ -404,7 +402,7 @@
    1.58    ;
    1.59    indcases (prop +)
    1.60    ;
    1.61 -  inductivecases thmdecl? (prop +) comment?
    1.62 +  inductivecases thmdecl? (prop +)
    1.63    ;
    1.64  
    1.65    rule: ('rule' ':' thmref)
    1.66 @@ -468,7 +466,7 @@
    1.67  
    1.68    dmspec: typespec '=' (cons + '|')
    1.69    ;
    1.70 -  cons: name (type * ) mixfix? comment?
    1.71 +  cons: name (type * ) mixfix?
    1.72    ;
    1.73    dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
    1.74  \end{rail}