
diff -r 7eb63f63e6c6 -r 279da0358aa9 doc-src/TutorialI/Misc/prime_def.thy
--- a/doc-src/TutorialI/Misc/prime_def.thy	Thu Jul 26 16:43:02 2001 +0200
+++ b/doc-src/TutorialI/Misc/prime_def.thy	Thu Jul 26 18:23:38 2001 +0200
@@ -1,6 +1,6 @@
 (*<*)
 theory prime_def = Main:;
-consts prime :: "nat \\<Rightarrow> bool"
+consts prime :: "nat \<Rightarrow> bool"
 (*>*)
 text{*
 \begin{warn}
@@ -8,6 +8,7 @@
 variables on the right-hand side.  Consider the following, flawed definition
 (where @{text"dvd"} means ``divides''):
 @{term[display,quotes]"prime(p) == 1 < p & (m dvd p --> (m=1 | m=p))"}
+\par\noindent\hangindent=0pt
 Isabelle rejects this ``definition'' because of the extra @{term"m"} on the
 right-hand side, which would introduce an inconsistency (why?). 
 The correct version is




