| changeset 29114 | 715178f6ae31 |
| parent 29112 | f2b45eea6dac |
| child 29560 | fa6c5d62adf5 |
| 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 |