src/Doc/IsarRef/Misc.thy

     @{command_def "unused_thms"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_facts"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
     @{command_def "print_binds"}@{text "\<^sup>*"} & : & @{text "context \<rightarrow>"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{command print_theory} | @@{command print_theorems}) ('!'?)
     ;
 
     @@{command find_theorems} ('(' @{syntax nat}? 'with_dups'? ')')? \<newline> (thmcriterion * )
     ;

       ('name' ':' @{syntax nameref} | 'strict' ':' @{syntax type} | @{syntax type})
     ;
     @@{command thm_deps} @{syntax thmrefs}
     ;
     @@{command unused_thms} ((@{syntax name} +) '-' (@{syntax name} * ))?
-  "}
+  \<close>}
 
   These commands print certain parts of the theory and proof context.
   Note that there are some further ones available, such as for the set
   of rules declared for simplifications.
 

     @{command_def "cd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "pwd"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
     @{command_def "use_thy"}@{text "\<^sup>*"} & : & @{text "any \<rightarrow>"} \\
   \end{matharray}
 
-  @{rail "
+  @{rail \<open>
     (@@{command cd} | @@{command use_thy}) @{syntax name}
-  "}
+  \<close>}
 
   \begin{description}
 
   \item @{command "cd"}~@{text path} changes the current directory
   of the Isabelle process.