doc-src/Ref/theory-syntax.tex
changeset 3130 1ffe03f4c700
parent 3108 335efc3f5632
child 3215 9e097d5cc246
equal deleted inserted replaced
3129:dd3666cbc764 3130:1ffe03f4c700
   125         ;
   125         ;
   126 
   126 
   127 instance : 'instance' ( name '<' name | name '::' arity) witness
   127 instance : 'instance' ( name '<' name | name '::' arity) witness
   128          ;
   128          ;
   129 
   129 
   130 witness : (() | ((string | longident) + ',')) (() | verbatim)
   130 witness : (() | '(' ((string | longident) + ',') ')') (() | verbatim)
   131         ;
   131         ;
   132 
   132 
   133 oracle : 'oracle' name
   133 oracle : 'oracle' name
   134        ;
   134        ;
   135 
   135