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