doc-src/IsarRef/Thy/Generic.thy

 
   Generic tools may refer to the information provided by object-logic
   declarations internally.
 
   @{rail "
-    @@{command judgment} @{syntax constdecl}
+    @@{command judgment} @{syntax name} '::' @{syntax type} @{syntax mixfix}?
     ;
     @@{attribute atomize} ('(' 'full' ')')?
     ;
     @@{attribute rule_format} ('(' 'noasm' ')')?
   "}