\begin{isabelle}% \isacommand{lemma}\ {"}n*n\ =\ n\ {\isasymLongrightarrow}\ n=0\ {\isasymor}\ n=1{"}\isanewline \end{isabelle}% %%% Local Variables: %%% mode: latex %%% TeX-master: "root" %%% End: