diff -r 8627da9246da -r b247e62520ec doc-src/TutorialI/Rules/Primes.thy
--- a/doc-src/TutorialI/Rules/Primes.thy	Mon Oct 23 17:37:03 2000 +0200
+++ b/doc-src/TutorialI/Rules/Primes.thy	Mon Oct 23 17:37:20 2000 +0200
@@ -2,9 +2,9 @@
 
 theory Primes = Main:
 consts
-  gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
+  gcd     :: "nat*nat \<Rightarrow> nat"               (*Euclid's algorithm *)
 
-recdef gcd "measure ((\<lambda>(m,n).n) ::nat*nat=>nat)"
+recdef gcd "measure ((\<lambda>(m,n).n) ::nat*nat \<Rightarrow> nat)"
     "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
 
 
@@ -89,7 +89,7 @@
 
 
 constdefs
-  is_gcd  :: "[nat,nat,nat]=>bool"        (*gcd as a relation*)
+  is_gcd  :: "[nat,nat,nat] \<Rightarrow> bool"        (*gcd as a relation*)
     "is_gcd p m n == p dvd m  \<and>  p dvd n  \<and>
                      (ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)"