doc-src/IsarRef/logics.tex

   \isarcmd{typedecl} & : & \isartrans{theory}{theory} \\
   \isarcmd{typedef} & : & \isartrans{theory}{proof(prove)} \\
 \end{matharray}
 
 \begin{rail}
-  'typedecl' typespec infix? comment?
-  ;
-  'typedef' parname? typespec infix? \\ '=' term comment?
+  'typedecl' typespec infix?
+  ;
+  'typedef' parname? typespec infix? '=' term
   ;
 \end{rail}
 
 \begin{descr}
 \item [$\isarkeyword{typedecl}~(\vec\alpha)t$] is similar to the original

   repdatatype (name * ) dtrules
   ;
 
   dtspec: parname? typespec infix? '=' (cons + '|')
   ;
-  cons: name (type * ) mixfix? comment?
+  cons: name (type * ) mixfix?
   ;
   dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
 \end{rail}
 
 \begin{descr}

 \railterm{recdeftc}
 
 \begin{rail}
   'primrec' parname? (equation + )
   ;
-  'recdef' ('(' 'permissive' ')')? \\ name term (eqn + ) hints?
-  ;
-  recdeftc thmdecl? tc comment?
-  ;
-
-  equation: thmdecl? eqn
-  ;
-  eqn: prop comment?
+  'recdef' ('(' 'permissive' ')')? \\ name term (prop + ) hints?
+  ;
+  recdeftc thmdecl? tc
+  ;
+
+  equation: thmdecl? prop
   ;
   hints: '(' 'hints' (recdefmod * ) ')'
   ;
   recdefmod: ((recdefsimp | recdefcong | recdefwf) (() | 'add' | 'del') ':' thmrefs) | clasimpmod
   ;

   ('inductive' | 'coinductive') sets intros monos?
   ;
   'mono' (() | 'add' | 'del')
   ;
 
-  sets: (term comment? +)
-  ;
-  intros: 'intros' (thmdecl? prop comment? +)
-  ;
-  monos: 'monos' thmrefs comment?
+  sets: (term +)
+  ;
+  intros: 'intros' (thmdecl? prop +)
+  ;
+  monos: 'monos' thmrefs
   ;
 \end{rail}
 
 \begin{descr}
 \item [$\isarkeyword{inductive}$ and $\isarkeyword{coinductive}$] define

   ;
   inducttac goalspec? (insts * 'and') rule?
   ;
   indcases (prop +)
   ;
-  inductivecases thmdecl? (prop +) comment?
+  inductivecases thmdecl? (prop +)
   ;
 
   rule: ('rule' ':' thmref)
   ;
 \end{rail}

   'domain' parname? (dmspec + 'and')
   ;
 
   dmspec: typespec '=' (cons + '|')
   ;
-  cons: name (type * ) mixfix? comment?
+  cons: name (type * ) mixfix?
   ;
   dtrules: 'distinct' thmrefs 'inject' thmrefs 'induction' thmrefs
 \end{rail}
 
 Recursive domains in HOLCF are analogous to datatypes in classical HOL (cf.\