diff -r 2896f88180b9 -r 8e1cae1de136 doc-src/IsarRef/logics.tex
--- a/doc-src/IsarRef/logics.tex	Tue Feb 12 20:32:23 2002 +0100
+++ b/doc-src/IsarRef/logics.tex	Tue Feb 12 20:33:03 2002 +0100
@@ -90,9 +90,9 @@
 \end{matharray}
 
 \begin{rail}
-  'typedecl' typespec infix? comment?
+  'typedecl' typespec infix?
   ;
-  'typedef' parname? typespec infix? \\ '=' term comment?
+  'typedef' parname? typespec infix? '=' term
   ;
 \end{rail}
 
@@ -186,7 +186,7 @@
 
   dtspec: parname? typespec infix? '=' (cons + '|')
   ;
-  cons: name (type * ) mixfix? comment?
+  cons: name (type * ) mixfix?
   ;
   dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
 \end{rail}
@@ -236,14 +236,12 @@
 \begin{rail}
   'primrec' parname? (equation + )
   ;
-  'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
+  'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
   ;
-  recdeftc thmdecl? tc comment?
+  recdeftc thmdecl? tc
   ;
 
-  equation: thmdecl? eqn
-  ;
-  eqn: prop comment?
+  equation: thmdecl? prop
   ;
   hints: '(' 'hints' (recdefmod * ) ')'
   ;
@@ -329,11 +327,11 @@
   'mono' (() | 'add' | 'del')
   ;
 
-  sets: (term comment? +)
+  sets: (term +)
   ;
-  intros: 'intros' (thmdecl? prop comment? +)
+  intros: 'intros' (thmdecl? prop +)
   ;
-  monos: 'monos' thmrefs comment?
+  monos: 'monos' thmrefs
   ;
 \end{rail}
 
@@ -404,7 +402,7 @@
   ;
   indcases (prop +)
   ;
-  inductivecases thmdecl? (prop +) comment?
+  inductivecases thmdecl? (prop +)
   ;
 
   rule: ('rule' ':' thmref)
@@ -468,7 +466,7 @@
 
   dmspec: typespec '=' (cons + '|')
   ;
-  cons: name (type * ) mixfix? comment?
+  cons: name (type * ) mixfix?
   ;
   dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
 \end{rail}