src/HOL/Word/Bit_Representation.thy

 lemma sbintrunc_bintrunc' [simp]:
   "0 < n \<Longrightarrow> sbintrunc (n - 1) (bintrunc n w) = sbintrunc (n - 1) w"
   by (cases n) (auto simp del: bintrunc.Suc)
 
 lemma bin_sbin_eq_iff: 
-  "bintrunc (Suc n) x = bintrunc (Suc n) y <-> 
+  "bintrunc (Suc n) x = bintrunc (Suc n) y \<longleftrightarrow> 
    sbintrunc n x = sbintrunc n y"
   apply (rule iffI)
    apply (rule box_equals [OF _ sbintrunc_bintrunc sbintrunc_bintrunc])
    apply simp
   apply (rule box_equals [OF _ bintrunc_sbintrunc bintrunc_sbintrunc])
   apply simp
   done
 
 lemma bin_sbin_eq_iff':
-  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y <-> 
+  "0 < n \<Longrightarrow> bintrunc n x = bintrunc n y \<longleftrightarrow> 
             sbintrunc (n - 1) x = sbintrunc (n - 1) y"
   by (cases n) (simp_all add: bin_sbin_eq_iff del: bintrunc.Suc)
 
 lemmas bintrunc_sbintruncS0 [simp] = bintrunc_sbintrunc' [unfolded One_nat_def]
 lemmas sbintrunc_bintruncS0 [simp] = sbintrunc_bintrunc' [unfolded One_nat_def]