doc-src/IsarRef/Thy/HOL_Specific.thy
changeset 29114 715178f6ae31
parent 29112 f2b45eea6dac
child 29560 fa6c5d62adf5
equal deleted inserted replaced
29113:fb31b7a6c858 29114:715178f6ae31
   810 
   810 
   811   \begin{rail}
   811   \begin{rail}
   812   'sledgehammer' (nameref *)
   812   'sledgehammer' (nameref *)
   813   ;
   813   ;
   814   'atp\_messages' ('(' nat ')')?
   814   'atp\_messages' ('(' nat ')')?
       
   815   ;
   815 
   816 
   816   'metis' thmrefs
   817   'metis' thmrefs
   817   ;
   818   ;
   818   \end{rail}
   819   \end{rail}
   819 
   820