src/HOL/Import/HOL/HOL4Vec.thy

  (%x::nat.
      (op -->::bool => bool => bool)
       ((op <::nat => nat => bool) x
         ((number_of::bin => nat)
           ((op BIT::bin => bool => bin)
-            ((op BIT::bin => bool => bin) (bin.Pls::bin) (True::bool))
+            ((op BIT::bin => bool => bin) (Numeral.Pls::bin) (True::bool))
             (False::bool))))
       ((op =::nat => nat => bool) ((BV::bool => nat) ((VB::nat => bool) x))
         x))"
   by (import bword_num BV_VB)
 

                                  k (0::nat) w2)))
                            ((BV::bool => nat) cin))
                          ((op ^::nat => nat => nat)
                            ((number_of::bin => nat)
                              ((op BIT::bin => bool => bin)
-                               ((op BIT::bin => bool => bin) (bin.Pls::bin)
+                               ((op BIT::bin => bool => bin) (Numeral.Pls::bin)
                                  (True::bool))
                                (False::bool)))
                            k)))))))"
   by (import bword_arith ACARRY_EQ_ADD_DIV)