--- a/doc-src/IsarRef/generic.tex Wed Nov 29 23:33:09 2006 +0100
+++ b/doc-src/IsarRef/generic.tex Thu Nov 30 14:17:22 2006 +0100
@@ -23,19 +23,21 @@
available, and result names need not be given.
\begin{rail}
- 'axiomatization' target? consts? ('where' specs)?
+ 'axiomatization' target? fixes? ('where' specs)?
;
- 'definition' target? (constdecl? constdef +)
+ 'definition' target? (decl 'where')? thmdecl? prop
;
- 'abbreviation' target? mode? (constdecl? prop +)
+ 'abbreviation' target? mode? (decl 'where')? prop
;
'notation' target? mode? (nameref mixfix + 'and')
;
- consts: ((name ('::' type)? structmixfix? | vars) + 'and')
+ fixes: ((name ('::' type)? mixfix? | vars) + 'and')
;
specs: (thmdecl? props + 'and')
;
+ decl: name ('::' type)? mixfix?
+ ;
\end{rail}
\begin{descr}