diff -r 966974a7a5b3 -r c613cd06d5cf doc-src/TutorialI/Misc/document/prime_def.tex
--- a/doc-src/TutorialI/Misc/document/prime_def.tex	Fri Jul 28 13:04:59 2000 +0200
+++ b/doc-src/TutorialI/Misc/document/prime_def.tex	Fri Jul 28 16:02:51 2000 +0200
@@ -1,14 +1,14 @@
 \begin{isabelle}%
 \isanewline
-~~~~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~((m~dvd~p)~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}%
+~~~~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~(m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}%
 \begin{isamarkuptext}%
 \noindent\small
 where \isa{dvd} means ``divides''.
 Isabelle rejects this ``definition'' because of the extra \isa{m} on the
-right-hand side, which would introduce an inconsistency. (Why?) What you
+right-hand side, which would introduce an inconsistency (why?). What you
 should have written is%
 \end{isamarkuptext}%
-~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~({\isasymforall}m.~(m~dvd~p)~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}\end{isabelle}%
+~{"}prime(p)~{\isasymequiv}~1~<~p~{\isasymand}~({\isasymforall}m.~m~dvd~p~{\isasymlongrightarrow}~(m=1~{\isasymor}~m=p)){"}\end{isabelle}%
 %%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "root"