HolSmt: don't get rid of quot and rem in arithmetic rules

It should not be necessary to rewrite these symbols with their
definitions, because from the perspective of SMT solvers, these should
just be functions like any others. Therefore, when replaying
arithmetic proof steps, the proof handler should not need to
understand what `quot` and `rem` are.

This is a partial revert of the following commit:
6220a17

It's not clear to me why I introduced this change in the first place,
since the tests do work fine without it. Also, there doesn't seem to
be any performance regression.

src/HolSmt/Z3_ProofReplay.sml

@@ -495,8 +495,7 @@ local
         PURE_REWRITE_TAC[integerTheory.EDIV_DEF, integerTheory.EMOD_DEF]
         (* the next rewrites are a workaround for this issue:
            https://github.com/HOL-Theorem-Prover/HOL/issues/1207 *)
-        >> PURE_REWRITE_TAC[integerTheory.INT_ABS, integerTheory.NUM_OF_INT,
-             integerTheory.int_quot, integerTheory.int_rem]
+        >> PURE_REWRITE_TAC[integerTheory.INT_ABS, integerTheory.NUM_OF_INT]
         (* if `arith_tactic` doesn't work at first, don't give up immediately;
            instead let's try additional tactics *)
         >> TRY arith_tactic