diff options
Diffstat (limited to 'backends/hol4/primitivesScript.sml')
| -rw-r--r-- | backends/hol4/primitivesScript.sml | 4 |
1 files changed, 2 insertions, 2 deletions
diff --git a/backends/hol4/primitivesScript.sml b/backends/hol4/primitivesScript.sml index 8cd54f33..7920454b 100644 --- a/backends/hol4/primitivesScript.sml +++ b/backends/hol4/primitivesScript.sml @@ -1624,8 +1624,8 @@ Proof prove_scalar_eq_equiv_tac QED -(* Remark.: don't move this up, it will break some proofs *) -val _ = BasicProvers.export_rewrites [ + +val _ = evalLib.add_rewrite_thms [ "isize_eq_equiv", "i8_eq_equiv", "i16_eq_equiv", |