1.1 --- a/doc-src/TutorialI/Rules/Primes.thy	Mon Oct 23 17:37:03 2000 +0200
     1.2 +++ b/doc-src/TutorialI/Rules/Primes.thy	Mon Oct 23 17:37:20 2000 +0200
     1.3 @@ -2,9 +2,9 @@
     1.4  
     1.5  theory Primes = Main:
     1.6  consts
     1.7 -  gcd     :: "nat*nat=>nat"               (*Euclid's algorithm *)
     1.8 +  gcd     :: "nat*nat \<Rightarrow> nat"               (*Euclid's algorithm *)
     1.9  
    1.10 -recdef gcd "measure ((\<lambda>(m,n).n) ::nat*nat=>nat)"
    1.11 +recdef gcd "measure ((\<lambda>(m,n).n) ::nat*nat \<Rightarrow> nat)"
    1.12      "gcd (m, n) = (if n=0 then m else gcd(n, m mod n))"
    1.13  
    1.14  
    1.15 @@ -89,7 +89,7 @@
    1.16  
    1.17  
    1.18  constdefs
    1.19 -  is_gcd  :: "[nat,nat,nat]=>bool"        (*gcd as a relation*)
    1.20 +  is_gcd  :: "[nat,nat,nat] \<Rightarrow> bool"        (*gcd as a relation*)
    1.21      "is_gcd p m n == p dvd m  \<and>  p dvd n  \<and>
    1.22                       (ALL d. d dvd m \<and> d dvd n \<longrightarrow> d dvd p)"
    1.23