doc-src/Ref/theory-syntax.tex
changeset 4543 82a45bdd0e80
parent 4317 7264fa2ff2ec
child 4891 19ff46cd2bad
--- a/doc-src/Ref/theory-syntax.tex	Thu Jan 08 19:04:33 1998 +0100
+++ b/doc-src/Ref/theory-syntax.tex	Fri Jan 09 13:49:20 1998 +0100
@@ -51,6 +51,8 @@
         | axclass
         | instance
         | oracle
+        | local
+        | global
         ;
 
 classes : 'classes' ( classDecl + )
@@ -118,7 +120,7 @@
 defs : 'defs' (( id string ) + )
      ;
 
-constdefs : 'constdefs' (id '::' (string | type) string +)
+constdefs : 'constdefs' (name '::' (string | type) string +)
           ;
 
 axclass : 'axclass' classDecl (() | ( id string ) +)
@@ -133,6 +135,12 @@
 oracle : 'oracle' name '=' name
        ;
 
+local : 'local'
+       ;
+
+global : 'global'
+       ;
+
 ml : 'ML' text
    ;