Remove the constant bit$LSB, which was simply arithmetic$ODD. This ma…

…y break some user proofs.

Also tidy-up bitScript and numeral_bitScript.

examples/ARM/v7/arm_stepScript.sml

@@ -798,8 +798,7 @@ val align_bx_bit = Q.store_thm("align_bx_bit",
    (!a:word32 n. (a || n2w n) ' 0 = a ' 0 \/ ODD n) /\
    (!a:word32 n. (a ?? n2w n) ' 0 = a ' 0 <> ODD n) /\
    (!a:word32 n. (a + n2w n) ' 0  = a ' 0 <> ODD n)`,
-  SRW_TAC [wordsLib.WORD_BIT_EQ_ss]
-    [WORD_ADD_BIT0, n2w_def, GSYM LSB_def, LSB_ODD]);
+  SRW_TAC [wordsLib.WORD_BIT_EQ_ss] [WORD_ADD_BIT0, n2w_def, BIT0_ODD]);
 
 val aligned_bx_thm = Q.store_thm("aligned_bx_thm",
   `!a:word32. aligned_bx a = (~a ' 0 ==> ~a ' 1)`,

src/emit/basis_emitScript.sml

@@ -974,7 +974,7 @@ val BITWISE_compute = Q.prove(
           (if opr (ODD a) (ODD b) then 1 else 0)`,
   Cases THEN1 REWRITE_TAC [CONJUNCT1 BITWISE_def]
     THEN REWRITE_TAC
-         [DIV2_def, NOT_SUC, PRE, EXP, BITWISE_EVAL, LSB_ODD, SBIT_def]);
+         [DIV2_def, NOT_SUC, PRE, EXP, BITWISE_EVAL, BIT0_ODD, SBIT_def]);
 
 val BIT_MODF_compute = Q.prove(
   `!n f x b e y.
@@ -1083,7 +1083,7 @@ val defs =
         BIT_MODF_compute, BIT_MODIFY_EVAL,
         BIT_REV_compute, BIT_REVERSE_EVAL,
         LOG2_compute, DIVMOD_2EXP, SBIT_def, BITS_def, MOD_2EXP_EQ_compute,
-        BITV_def, BIT_def, SLICE_def, LSB_def, SIGN_EXTEND_def, BOOLIFY_compute]
+        BITV_def, BIT_def, SLICE_def, SIGN_EXTEND_def, BOOLIFY_compute]
 
 val _ = eSML "bit"
   (MLSIG  "type num = numML.num" ::