src/HOL/Word/BinBoolList.thy

   Nil: "rbl_mult Nil x = Nil"
   | Cons: "rbl_mult (y # ys) x = (let ws = False # rbl_mult ys x in 
     if y then rbl_add ws x else ws)"
 
 lemma butlast_power:
-  "(butlast ^ n) bl = take (length bl - n) bl"
+  "(butlast o^ n) bl = take (length bl - n) bl"
   by (induct n) (auto simp: butlast_take)
 
 lemma bin_to_bl_aux_Pls_minus_simp [simp]:
   "0 < n ==> bin_to_bl_aux n Int.Pls bl = 
     bin_to_bl_aux (n - 1) Int.Pls (False # bl)"

   apply (cases "k <= length bl")
    apply auto
   done
 
 lemma nth_rest_power_bin [rule_format] :
-  "ALL n. bin_nth ((bin_rest ^ k) w) n = bin_nth w (n + k)"
+  "ALL n. bin_nth ((bin_rest o^ k) w) n = bin_nth w (n + k)"
   apply (induct k, clarsimp)
   apply clarsimp
   apply (simp only: bin_nth.Suc [symmetric] add_Suc)
   done
 
 lemma take_rest_power_bin:
-  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest ^ (n - m)) w)" 
+  "m <= n ==> take m (bin_to_bl n w) = bin_to_bl m ((bin_rest o^ (n - m)) w)" 
   apply (rule nth_equalityI)
    apply simp
   apply (clarsimp simp add: nth_bin_to_bl nth_rest_power_bin)
   done