--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/doc-src/TutorialI/Misc/document/arith3.tex Wed Apr 19 12:59:38 2000 +0200
@@ -0,0 +1,3 @@
+\begin{isabelle}%
+\isacommand{lemma}~{"}n*n~=~n~{\isasymLongrightarrow}~n=0~{\isasymor}~n=1{"}\isanewline
+\end{isabelle}%