
diff -r f6b0d827240e -r bdc1e2f0a86a src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Tue Sep 01 17:25:36 2015 +0200
+++ b/src/HOL/Divides.thy	Tue Sep 01 22:32:58 2015 +0200
@@ -814,8 +814,8 @@
 text \<open>
   We define @{const divide} and @{const mod} on @{typ nat} by means
   of a characteristic relation with two input arguments
-  @{term "m\<Colon>nat"}, @{term "n\<Colon>nat"} and two output arguments
-  @{term "q\<Colon>nat"}(uotient) and @{term "r\<Colon>nat"}(emainder).
+  @{term "m::nat"}, @{term "n::nat"} and two output arguments
+  @{term "q::nat"}(uotient) and @{term "r::nat"}(emainder).
 \<close>
 
 definition divmod_nat_rel :: "nat \<Rightarrow> nat \<Rightarrow> nat \<times> nat \<Rightarrow> bool" where
@@ -835,7 +835,7 @@
   have "\<exists>q r. m = q * n + r \<and> r < n"
   proof (induct m)
     case 0 with \<open>n \<noteq> 0\<close>
-    have "(0\<Colon>nat) = 0 * n + 0 \<and> 0 < n" by simp
+    have "(0::nat) = 0 * n + 0 \<and> 0 < n" by simp
     then show ?case by blast
   next
     case (Suc m) then obtain q' r'
@@ -868,7 +868,7 @@
       (simp add: divmod_nat_rel_def)
 next
   case False
-  have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q\<Colon>nat)"
+  have aux: "\<And>q r q' r'. q' * n + r' = q * n + r \<Longrightarrow> r < n \<Longrightarrow> q' \<le> (q::nat)"
   apply (rule leI)
   apply (subst less_iff_Suc_add)
   apply (auto simp add: add_mult_distrib)
@@ -1115,10 +1115,10 @@
   then show "m div n * n + m mod n \<le> m" by auto
 qed
 
-lemma mod_geq: "\<not> m < (n\<Colon>nat) \<Longrightarrow> m mod n = (m - n) mod n"
+lemma mod_geq: "\<not> m < (n::nat) \<Longrightarrow> m mod n = (m - n) mod n"
 by (simp add: le_mod_geq linorder_not_less)
 
-lemma mod_if: "m mod (n\<Colon>nat) = (if m < n then m else (m - n) mod n)"
+lemma mod_if: "m mod (n::nat) = (if m < n then m else (m - n) mod n)"
 by (simp add: le_mod_geq)
 
 lemma mod_1 [simp]: "m mod Suc 0 = 0"
@@ -1313,7 +1313,7 @@
 
 lemma split_div_lemma:
   assumes "0 < n"
-  shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m\<Colon>nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
+  shows "n * q \<le> m \<and> m < n * Suc q \<longleftrightarrow> q = ((m::nat) div n)" (is "?lhs \<longleftrightarrow> ?rhs")
 proof
   assume ?rhs
   with mult_div_cancel have nq: "n * q = m - (m mod n)" by simp
@@ -1486,7 +1486,7 @@
 lemma add_self_div_2 [simp]: "(m + m) div 2 = (m::nat)"
 by (simp add: mult_2 [symmetric])
 
-lemma mod2_gr_0 [simp]: "0 < (m\<Colon>nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
+lemma mod2_gr_0 [simp]: "0 < (m::nat) mod 2 \<longleftrightarrow> m mod 2 = 1"
 proof -
   { fix n :: nat have  "(n::nat) < 2 \<Longrightarrow> n = 0 \<or> n = 1" by (cases n) simp_all }
   moreover have "m mod 2 < 2" by simp
@@ -1999,7 +1999,7 @@
 lemmas zmod_eq_0D [dest!] = zmod_eq_0_iff [THEN iffD1]
 
 lemma zmod_zdiv_equality' [nitpick_unfold]:
-  "(m\<Colon>int) mod n = m - (m div n) * n"
+  "(m::int) mod n = m - (m div n) * n"
   using mod_div_equality [of m n] by arith
 
 




