doc-src/IsarRef/syntax.tex

--- a/doc-src/IsarRef/syntax.tex	Fri Jul 30 14:59:32 1999 +0200
+++ b/doc-src/IsarRef/syntax.tex	Fri Jul 30 15:40:54 1999 +0200
@@ -74,6 +74,7 @@
 ever refer to sorts or arities explicitly.
 
 \indexouternonterm{sort}\indexouternonterm{arity}\indexouternonterm{simplearity}
+\indexouternonterm{classdecl}
 \begin{rail}
   sort : nameref | lbrace (nameref * ',') rbrace
   ;
@@ -81,6 +82,7 @@
   ;
   simplearity : ( () | '(' (sort + ',') ')' ) nameref
   ;
+  classdecl: name ('<' (nameref ',' +))? comment?
 \end{rail}
 
 
@@ -181,10 +183,13 @@
 as proof method arguments).  Any of these may include lists of attributes,
 which are applied to the preceding theorem or list of theorems.
 
-\indexouternonterm{thmdecl}\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
+\indexouternonterm{thmdecl}\indexouternonterm{axmdecl}
+\indexouternonterm{thmdef}\indexouternonterm{thmrefs}
 \begin{rail}
   thmname : name attributes | name | attributes
   ;
+  axmdecl : name attributes? ':'
+  ;
   thmdecl : thmname ':'
   ;
   thmdef : thmname '='