--- 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}