doc-src/IsarRef/Thy/document/Generic.tex

 
   Generic tools may refer to the information provided by object-logic
   declarations internally.
 
   \begin{railoutput}
-\rail@begin{1}{}
+\rail@begin{2}{}
 \rail@term{\hyperlink{command.judgment}{\mbox{\isa{\isacommand{judgment}}}}}[]
-\rail@nont{\hyperlink{syntax.constdecl}{\mbox{\isa{constdecl}}}}[]
+\rail@nont{\hyperlink{syntax.name}{\mbox{\isa{name}}}}[]
+\rail@term{\isa{{\isaliteral{3A}{\isacharcolon}}{\isaliteral{3A}{\isacharcolon}}}}[]
+\rail@nont{\hyperlink{syntax.type}{\mbox{\isa{type}}}}[]
+\rail@bar
+\rail@nextbar{1}
+\rail@nont{\hyperlink{syntax.mixfix}{\mbox{\isa{mixfix}}}}[]
+\rail@endbar
 \rail@end
 \rail@begin{2}{}
 \rail@term{\hyperlink{attribute.atomize}{\mbox{\isa{atomize}}}}[]
 \rail@bar
 \rail@nextbar{1}