diff -r 778f0897e7e5 -r 78dfc5904eea doc-src/TutorialI/Rules/rules.tex
--- a/doc-src/TutorialI/Rules/rules.tex	Fri Jan 05 15:39:34 2001 +0100
+++ b/doc-src/TutorialI/Rules/rules.tex	Fri Jan 05 18:16:01 2001 +0100
@@ -1,3 +1,4 @@
+% $Id$
 \chapter{The Rules of the Game}
 \label{chap:rules}
  
@@ -1314,10 +1315,8 @@
 \begin{isabelle}
 \isacommand{lemma}\ gcd_greatest\
 [rule_format]:\isanewline
-\ \ \ \ \ \ \ "(k\ dvd\
-m)\ \isasymlongrightarrow\ (k\ dvd\
-n)\ \isasymlongrightarrow\ k\ dvd\
-gcd(m,n)"\isanewline
+\ \ \ \ \ \ \ "k\ dvd\ m\ \isasymlongrightarrow\ k\ dvd\ n\ \isasymlongrightarrow\
+k\ dvd\ gcd(m,n)"\isanewline
 \isacommand{apply}\ (induct_tac\ m\ n\
 rule:\ gcd.induct)\isanewline
 \isacommand{apply}\ (case_tac\ "n=0")\isanewline
@@ -1338,7 +1337,8 @@
 of \isa{blast}, and it is worth doing for sound logical reasons.
 \begin{isabelle}
 \isacommand{theorem}\ gcd_greatest_iff\ [iff]:\isanewline
-\ \ \ \ \ \ \ \ \ "k\ dvd\ gcd(m,n)\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\ n)"\isanewline
+\ \ \ \ \ \ \ \ \ "(k\ dvd\ gcd(m,n))\ =\ (k\ dvd\ m\ \isasymand\ k\ dvd\
+n)"\isanewline
 \isacommand{apply}\ (blast\ intro!:\ gcd_greatest\ intro:\ dvd_trans)\isanewline
 \isacommand{done}
 \end{isabelle}