diff options
Diffstat (limited to 'backends/hol4/Test.sml')
| -rw-r--r-- | backends/hol4/Test.sml | 7 |
1 files changed, 2 insertions, 5 deletions
diff --git a/backends/hol4/Test.sml b/backends/hol4/Test.sml index b16b67fb..61d0706d 100644 --- a/backends/hol4/Test.sml +++ b/backends/hol4/Test.sml @@ -168,11 +168,8 @@ val i32_to_int_bounds = "i32_to_int_bounds", “!n. i32_min <= i32_to_int n /\ i32_to_int n <= i32_max”) -val int_to_u32_id = - new_axiom ( - "int_to_u32_id", - “!n. 0 <= n /\ n <= u32_max ==> - u32_to_int (int_to_u32 n) = n”) +val int_to_u32_id = new_axiom ("int_to_u32_id", + “!n. 0 <= n /\ n <= u32_max ==> u32_to_int (int_to_u32 n) = n”) val int_to_i32_id = new_axiom ( |