unsymbolized;

--- a/src/HOL/NumberTheory/IntPrimes.ML	Tue Oct 03 18:56:44 2000 +0200
+++ b/src/HOL/NumberTheory/IntPrimes.ML	Tue Oct 03 18:57:11 2000 +0200
@@ -28,7 +28,7 @@
 by (simp_tac (simpset() addsimps [gcd_commute]) 1); 
 qed "gcd_add1_eq";
 
-Goal "m <= n \\<Longrightarrow> gcd (n, n - m) = gcd (n, m)";
+Goal "m <= n ==> gcd (n, n - m) = gcd (n, m)";
 by (subgoal_tac "n = m + (n-m)" 1);
 by (etac ssubst 1 THEN rtac gcd_add1_eq 1);
 by (Asm_simp_tac 1);
@@ -672,7 +672,7 @@
 val [xzgcda_eq] = xzgcda.simps;
 Delsimps xzgcda.simps;
 
-Goal "zgcd(r',r) = k --> #0 < r \\<longrightarrow> \
+Goal "zgcd(r',r) = k --> #0 < r --> \
 \     (EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn))";
 by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
                   ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
@@ -691,7 +691,7 @@
 by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); 
 val lemma1 = result();
 
-Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) --> #0 < r \\<longrightarrow>  \
+Goal "(EX sn tn. xzgcda (m,n,r',r,s',s,t',t) = (k,sn,tn)) --> #0 < r --> \
 \     zgcd(r',r) = k";
 by (res_inst_tac [("u","m"),("v","n"),("w","r'"),("x","r"),
                   ("y","s'"),("z","s"),("aa","t'"),("ab","t")] 
@@ -709,7 +709,7 @@
 by (asm_full_simp_tac (simpset() addsimps [zabs_def]) 1); 
 val lemma2 = result();
 
-Goalw [xzgcd_def] "#0 < n \\<Longrightarrow> (zgcd(m,n) = k) = (EX s t. xzgcd m n = (k,s,t))"; 
+Goalw [xzgcd_def] "#0 < n ==> (zgcd(m,n) = k) = (EX s t. xzgcd m n = (k,s,t))"; 
 by (rtac iffI 1);
 by (rtac (lemma2 RS mp RS mp) 2);
 by (rtac (lemma1 RS mp RS mp) 1);

--- a/src/HOL/NumberTheory/Primes.thy	Tue Oct 03 18:56:44 2000 +0200
+++ b/src/HOL/NumberTheory/Primes.thy	Tue Oct 03 18:57:11 2000 +0200
@@ -1,4 +1,4 @@
-(*  Title:      HOL/ex/Primes.thy
+(*  Title:      HOL/NumberTheory/Primes.thy
     ID:         $Id$
     Author:     Christophe Tabacznyj and Lawrence C Paulson
     Copyright   1996  University of Cambridge
@@ -149,7 +149,7 @@
   apply (simp)
   done
 
-lemma relprime_dvd_mult_iff: "gcd(k,n)=1 \<Longrightarrow> k dvd (m*n) = k dvd m";
+lemma relprime_dvd_mult_iff: "gcd(k,n)=1 ==> k dvd (m*n) = k dvd m";
   apply (blast intro: relprime_dvd_mult dvd_trans)
   done