diff -r 97c06cfd31e5 -r 31f2105521ee src/HOL/Word/Word.thy
--- a/src/HOL/Word/Word.thy	Sun Dec 27 16:40:09 2015 +0100
+++ b/src/HOL/Word/Word.thy	Sun Dec 27 17:16:21 2015 +0100
@@ -1425,7 +1425,7 @@
   apply force
   done
 
-lemma udvd_iff_dvd: "x udvd y <-> unat x dvd unat y"
+lemma udvd_iff_dvd: "x udvd y \<longleftrightarrow> unat x dvd unat y"
   unfolding dvd_def udvd_nat_alt by force
 
 lemmas unat_mono = word_less_nat_alt [THEN iffD1]
@@ -3273,7 +3273,7 @@
 lemma eq_mod_iff: "0 < (n::int) \<Longrightarrow> b = b mod n \<longleftrightarrow> 0 \<le> b \<and> b < n"
   by (simp add: int_mod_lem eq_sym_conv)
 
-lemma mask_eq_iff: "(w AND mask n) = w <-> uint w < 2 ^ n"
+lemma mask_eq_iff: "(w AND mask n) = w \<longleftrightarrow> uint w < 2 ^ n"
   apply (simp add: and_mask_bintr)
   apply (simp add: word_ubin.inverse_norm)
   apply (simp add: eq_mod_iff bintrunc_mod2p min_def)
@@ -3691,7 +3691,7 @@
   done
 
 lemma word_split_bl: "std = size c - size b \<Longrightarrow> 
-    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) <-> 
+    (a = of_bl (take std (to_bl c)) & b = of_bl (drop std (to_bl c))) \<longleftrightarrow> 
     word_split c = (a, b)"
   apply (rule iffI)
    defer
@@ -3729,7 +3729,7 @@
     (\<forall>n::nat. b !! n \<longleftrightarrow> n < size b \<and> c !! n) \<and> (\<forall>m::nat. a !! m \<longleftrightarrow> m < size a \<and> c !! (m + size b))"
   by (simp add: test_bit_split')
 
-lemma test_bit_split_eq: "word_split c = (a, b) <-> 
+lemma test_bit_split_eq: "word_split c = (a, b) \<longleftrightarrow> 
   ((ALL n::nat. b !! n = (n < size b & c !! n)) &
     (ALL m::nat. a !! m = (m < size a & c !! (m + size b))))"
   apply (rule_tac iffI)